===========================================================
.___ __ __
_________________ __ __ __| _/|__|/ |_
/ ___\_` __ \__ \ | | \/ __ | | \\_ __\
/ /_/ > | \// __ \| | / /_/ | | || |
\___ /|__| (____ /____/\____ | |__||__|
/_____/ \/ \/
grep rough audit - static analysis tool
v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
hol88-2.02.19940316/lisp/f-cl.l-384-
hol88-2.02.19940316/lisp/f-cl.l:385:(defmacro cadaddr (x) `(car (cdaddr ,x)))
hol88-2.02.19940316/lisp/f-cl.l:386:(defmacro cadddaddr (x) `(caddr (cdaddr ,x)))
hol88-2.02.19940316/lisp/f-cl.l:387:(defmacro caddaddr (x) `(cadr (cdaddr ,x)))
hol88-2.02.19940316/lisp/f-cl.l:388:(defmacro caddadadr (x) `(caddr (cadadr ,x)))
hol88-2.02.19940316/lisp/f-cl.l-389-(defmacro cadadadr (x) `(cadr (cadadr ,x)))
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-1980-#define MMcadar(x) (x)->c.c_car->c.c_cdr->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c:1981:#define MMcaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c-1982-#define MMcdaar(x) (x)->c.c_car->c.c_car->c.c_cdr
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-1988-#define MMcaadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c:1989:#define MMcaaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c-1990-#define MMcadaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_car
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-1996-#define MMcdadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/lisp/f-ol-syntax.c:1997:#define MMcdaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/lisp/f-ol-syntax.c-1998-#define MMcddaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_cdr
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-2322-object cadar();
hol88-2.02.19940316/lisp/f-ol-syntax.c:2323:object caddr();
hol88-2.02.19940316/lisp/f-ol-syntax.c-2324-object cdaar();
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-2330-object caadar();
hol88-2.02.19940316/lisp/f-ol-syntax.c:2331:object caaddr();
hol88-2.02.19940316/lisp/f-ol-syntax.c-2332-object cadaar();
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-2338-object cdadar();
hol88-2.02.19940316/lisp/f-ol-syntax.c:2339:object cdaddr();
hol88-2.02.19940316/lisp/f-ol-syntax.c-2340-object cddaar();
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-3222-#define Mcadar(x) (x)->c.c_car->c.c_cdr->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c:3223:#define Mcaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c-3224-#define Mcdaar(x) (x)->c.c_car->c.c_car->c.c_cdr
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-3230-#define Mcaadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c:3231:#define Mcaaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c-3232-#define Mcadaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_car
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-3238-#define Mcdadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/lisp/f-ol-syntax.c:3239:#define Mcdaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/lisp/f-ol-syntax.c-3240-#define Mcddaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_cdr
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-3255-#define CMPcadar(x) (x)->c.c_car->c.c_cdr->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c:3256:#define CMPcaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c-3257-#define CMPcdaar(x) (x)->c.c_car->c.c_car->c.c_cdr
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-3263-#define CMPcaadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c:3264:#define CMPcaaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/lisp/f-ol-syntax.c-3265-#define CMPcadaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_car
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-3271-#define CMPcdadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/lisp/f-ol-syntax.c:3272:#define CMPcdaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/lisp/f-ol-syntax.c-3273-#define CMPcddaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_cdr
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-4873-void Lcadadr(void);
hol88-2.02.19940316/lisp/f-ol-syntax.c:4874:void Lcaaddr(void);
hol88-2.02.19940316/lisp/f-ol-syntax.c-4875-void Lset_macro_character(void);
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-4986-void Lcddadr(void);
hol88-2.02.19940316/lisp/f-ol-syntax.c:4987:void Lcdaddr(void);
hol88-2.02.19940316/lisp/f-ol-syntax.c-4988-void Lcadddr(void);
##############################################
hol88-2.02.19940316/lisp/f-ol-syntax.c-5163-void Lcdadr(void);
hol88-2.02.19940316/lisp/f-ol-syntax.c:5164:void Lcaddr(void);
hol88-2.02.19940316/lisp/f-ol-syntax.c-5165-void Lfmakunbound(void);
##############################################
hol88-2.02.19940316/ml/drul.ml-744- let th1 = EXISTS (mk_exists(x,cncl),x) (UNDISCH th) in
hol88-2.02.19940316/ml/drul.ml:745: let asm = mk_exists(x,ante) in
hol88-2.02.19940316/ml/drul.ml:746: DISCH asm (CHOOSE (x,ASSUME asm) th1) ?
hol88-2.02.19940316/ml/drul.ml-747- failwith `EXISTS_IMP: variable free in assumptions`;;
##############################################
hol88-2.02.19940316/ml/conv.ml-1121- if fP then
hol88-2.02.19940316/ml/conv.ml:1122: let asm = mk_exists(x,P) in
hol88-2.02.19940316/ml/conv.ml-1123- let th1 = CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm))) in
hol88-2.02.19940316/ml/conv.ml:1124: let imp1 = DISCH tm (DISCH asm th1) in
hol88-2.02.19940316/ml/conv.ml-1125- let cncl = rand(concl imp1) in
##############################################
hol88-2.02.19940316/ml/conv.ml-1133- IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH cncl imp2) else
hol88-2.02.19940316/ml/conv.ml:1134: let asm = mk_exists(x,P) in
hol88-2.02.19940316/ml/conv.ml-1135- let th1 = GEN x (CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm)))) in
hol88-2.02.19940316/ml/conv.ml:1136: let imp1 = DISCH tm (DISCH asm th1) in
hol88-2.02.19940316/ml/conv.ml-1137- let cncl = rand(concl imp1) in
##############################################
hol88-2.02.19940316/ml/conv.ml-1378- let imp1 = DISCH_ALL (GEN x (AP_THM (ASSUME tm) x)) in
hol88-2.02.19940316/ml/conv.ml:1379: let asm = ASSUME (concl (GEN x (AP_THM (ASSUME tm) x))) in
hol88-2.02.19940316/ml/conv.ml-1380- IMP_ANTISYM_RULE imp1 (DISCH_ALL (EXT asm))
##############################################
hol88-2.02.19940316/ml/conv.ml-1401- let imp1 = DISCH_ALL (GEN x (AP_THM (ASSUME tm) x)) in
hol88-2.02.19940316/ml/conv.ml:1402: let asm = ASSUME (concl (GEN x (AP_THM (ASSUME tm) x))) in
hol88-2.02.19940316/ml/conv.ml-1403- IMP_ANTISYM_RULE imp1 (DISCH_ALL (EXT asm))) ?\st
##############################################
hol88-2.02.19940316/ml/tyfns.ml-203- let thm2 = GENL ov (DISCH hy thm1) in
hol88-2.02.19940316/ml/tyfns.ml:204: let asm = concl thm2 in
hol88-2.02.19940316/ml/tyfns.ml-205- let thm3 = SPECL iv (UNDISCH (SPECL ov (ASSUME asm))) in
hol88-2.02.19940316/ml/tyfns.ml-206- let thm4 = GENL vs (DISCH hy thm3) in
hol88-2.02.19940316/ml/tyfns.ml:207: IMP_ANTISYM_RULE (DISCH tm thm2) (DISCH asm thm4);;
hol88-2.02.19940316/ml/tyfns.ml-208-
##############################################
hol88-2.02.19940316/ml/tyfns.ml-531- r2 = REWR_CONV fndef (mk_comb(fn,C')) and
hol88-2.02.19940316/ml/tyfns.ml:532: asm = AP_TERM fn (ASSUME (mk_eq(C,C'))) and
hol88-2.02.19940316/ml/tyfns.ml-533- v1 = genvar tupty and v2 = genvar tupty in
##############################################
hol88-2.02.19940316/ml/tyfns.ml-616- let rule fn eth th =
hol88-2.02.19940316/ml/tyfns.ml:617: let asm = (mk_eq o (rand # rand))(dest_eq(fst(dest_imp(concl th)))) in
hol88-2.02.19940316/ml/tyfns.ml:618: let imp = (IMP_TRANS (DISCH asm (AP_TERM fn (ASSUME asm))) th) in
hol88-2.02.19940316/ml/tyfns.ml-619- GEN_ALL (NOT_INTRO(CHOOSE (fn,eth) imp)) in
##############################################
hol88-2.02.19940316/ml/tyfns.ml-639- let rots = mk_rot (map (C SPEC lemma) nums) in
hol88-2.02.19940316/ml/tyfns.ml:640: let fn,asm = dest_exists(concl eth) in
hol88-2.02.19940316/ml/tyfns.ml-641- let fneqs = map (SYM o SPEC_ALL) (CONJUNCTS (ASSUME asm)) in
##############################################
hol88-2.02.19940316/ml/tydefs.ml-531- let chfn fn v th =
hol88-2.02.19940316/ml/tydefs.ml:532: let asm = ASSUME (mk_exists(v,find fn (hyp th))) in
hol88-2.02.19940316/ml/tydefs.ml-533- CHOOSE (v,asm) th in
##############################################
hol88-2.02.19940316/ml/tydefs.ml-543- let a1,a2 = CONJ_PAIR(ASSUME ANTE) in
hol88-2.02.19940316/ml/tydefs.ml:544: let asm = MP (SPEC tl (ASSUME res)) a2 in
hol88-2.02.19940316/ml/tydefs.ml-545- let thm4 = SUBST [SYM (ASSUME def),v] Q (SPECL vs asm) in
##############################################
hol88-2.02.19940316/ml/list.ml-54- let base' = EQ_MP (SYM(BETA_CONV "^P []")) base and
hol88-2.02.19940316/ml/list.ml:55: step' = DISCH asm (SPEC h (UNDISCH(SPEC tl step))) and
hol88-2.02.19940316/ml/list.ml-56- hypth = SYM(RIGHT_BETA(REFL "^P ^tl")) and
##############################################
hol88-2.02.19940316/ml/hol-drule.ml-1693- let imp2 =
hol88-2.02.19940316/ml/hol-drule.ml:1694: let asm = ASSUME "^t1 \/ ^t2" in
hol88-2.02.19940316/ml/hol-drule.ml-1695- let a1 = CONJUNCT1(ASSUME "~^t1 /\ ~^t2") and
hol88-2.02.19940316/ml/hol-drule.ml-1696- a2 = CONJUNCT2(ASSUME "~^t1 /\ ~^t2") in
hol88-2.02.19940316/ml/hol-drule.ml:1697: let fth = DISJ_CASES asm (UNDISCH a1) (UNDISCH a2) in
hol88-2.02.19940316/ml/hol-drule.ml-1698- DISCH "~^t1 /\ ~^t2" (NOT_INTRO(DISCH "^t1 \/ ^t2" fth)) in
##############################################
hol88-2.02.19940316/theories/mk_BASIC-HOL.ml-67- let def = EQ_MP th2 th1 in
hol88-2.02.19940316/theories/mk_BASIC-HOL.ml:68: let asm = ASSUME (snd(dest_exists(concl def))) in
hol88-2.02.19940316/theories/mk_BASIC-HOL.ml-69- let (asm1,asm2) = (CONJUNCT1 asm, CONJUNCT2 asm) in
##############################################
hol88-2.02.19940316/theories/mk_ltree.ml-103- let (asm,con) = (dest_imp body) in
hol88-2.02.19940316/theories/mk_ltree.ml:104: let ALL_EL,[P;tll] = strip_comb asm in
hol88-2.02.19940316/theories/mk_ltree.ml-105- let b = genvar bool_ty in
##############################################
hol88-2.02.19940316/theories/mk_ltree.ml-129- let trl = variant ((frees body') @ (freesl A)) "trl:(tree)list" in
hol88-2.02.19940316/theories/mk_ltree.ml:130: let asm = "ALL_EL (\^t'.^body') trl" in
hol88-2.02.19940316/theories/mk_ltree.ml-131- ([ (asm.A, subst["node ^trl",t']body')],
hol88-2.02.19940316/theories/mk_ltree.ml:132: \[thm]. tree_INDUCT (GEN trl (DISCH asm thm)))
hol88-2.02.19940316/theories/mk_ltree.ml-133- ) ? failwith `tree_INDUCT_TAC`;;
##############################################
hol88-2.02.19940316/theories/mk_ltree.ml-601- let (asm,v,con) = (I # dest_forall) (dest_imp body) in
hol88-2.02.19940316/theories/mk_ltree.ml:602: let ALL_EL,[P;tll] = strip_comb asm in
hol88-2.02.19940316/theories/mk_ltree.ml-603- let b = genvar bool_ty in
##############################################
hol88-2.02.19940316/theories/mk_ltree.ml-605- IND = SPEC P (INST_TYPE [type_of v,":*"] ltree_Induct) and
hol88-2.02.19940316/theories/mk_ltree.ml:606: th' = DISCH asm (SPEC v (UNDISCH(SPEC tl th))) in
hol88-2.02.19940316/theories/mk_ltree.ml-607- let th1 = SUBST [concth,b]
##############################################
hol88-2.02.19940316/theories/mk_ltree.ml-609- (REFL (concl th')) in
hol88-2.02.19940316/theories/mk_ltree.ml:610: let th2 = GEN tl (DISCH asm (GEN v(UNDISCH (EQ_MP th1 th')))) in
hol88-2.02.19940316/theories/mk_ltree.ml-611- CONV_RULE (ONCE_DEPTH_CONV BETA_CONV) (MP IND th2)?failwith `ltree_INDUCT`);;
##############################################
hol88-2.02.19940316/theories/mk_ltree.ml-630- let trl = variant ((frees body') @ (freesl A)) "trl:((^t_ty)ltree)list" in
hol88-2.02.19940316/theories/mk_ltree.ml:631: let asm = "ALL_EL (\^t'.^body') trl" in
hol88-2.02.19940316/theories/mk_ltree.ml-632- ([ (asm.A, mk_forall (v',subst["Node (^v') ^trl",t']body'))],
hol88-2.02.19940316/theories/mk_ltree.ml:633: \[thm]. ltree_INDUCT (GEN trl (DISCH asm thm)))
hol88-2.02.19940316/theories/mk_ltree.ml-634- ) ? failwith `ltree_INDUCT_TAC`;;
##############################################
hol88-2.02.19940316/theories/mk_tydefs.ml-73- let (asm,v,con) = (I # dest_forall) (dest_imp body) in
hol88-2.02.19940316/theories/mk_tydefs.ml:74: let ALL_EL,[P;tll] = strip_comb asm in
hol88-2.02.19940316/theories/mk_tydefs.ml-75- let b = genvar bool_ty in
##############################################
hol88-2.02.19940316/theories/mk_tydefs.ml-77- IND = SPEC P (INST_TYPE [type_of v,":*"] ltree_Induct) and
hol88-2.02.19940316/theories/mk_tydefs.ml:78: th' = DISCH asm (SPEC v (UNDISCH(SPEC tl th))) in
hol88-2.02.19940316/theories/mk_tydefs.ml-79- let th1 = SUBST [concth,b]
##############################################
hol88-2.02.19940316/theories/mk_tydefs.ml-81- (REFL (concl th')) in
hol88-2.02.19940316/theories/mk_tydefs.ml:82: let th2 = GEN tl (DISCH asm (GEN v(UNDISCH (EQ_MP th1 th')))) in
hol88-2.02.19940316/theories/mk_tydefs.ml-83- CONV_RULE (ONCE_DEPTH_CONV BETA_CONV) (MP IND th2) ?
##############################################
hol88-2.02.19940316/theories/mk_tydefs.ml-103- let trl = variant ((frees body') @ (freesl A)) "trl:((^t_ty)ltree)list" in
hol88-2.02.19940316/theories/mk_tydefs.ml:104: let asm = "ALL_EL (\^t'.^body') trl" in
hol88-2.02.19940316/theories/mk_tydefs.ml-105- ([ (asm.A, mk_forall (v',subst["Node (^v') ^trl",t']body'))],
hol88-2.02.19940316/theories/mk_tydefs.ml:106: \[thm]. ltree_INDUCT (GEN trl (DISCH asm thm)))
hol88-2.02.19940316/theories/mk_tydefs.ml-107- ) ? failwith `ltree_INDUCT_TAC`;;
##############################################
hol88-2.02.19940316/theories/mk_tree.ml-516- let (asm,con) = (dest_imp body) in
hol88-2.02.19940316/theories/mk_tree.ml:517: let ALL_EL,[P;tll] = strip_comb asm in
hol88-2.02.19940316/theories/mk_tree.ml-518- let b = genvar bool_ty in
##############################################
hol88-2.02.19940316/theories/mk_tree.ml-542- let trl = variant ((frees body') @ (freesl A)) "trl:(tree)list" in
hol88-2.02.19940316/theories/mk_tree.ml:543: let asm = "ALL_EL (\^t'.^body') trl" in
hol88-2.02.19940316/theories/mk_tree.ml-544- ([ (asm.A, subst["node ^trl",t']body')],
hol88-2.02.19940316/theories/mk_tree.ml:545: \[thm]. tree_INDUCT (GEN trl (DISCH asm thm)))
hol88-2.02.19940316/theories/mk_tree.ml-546- ) ? failwith `tree_INDUCT_TAC`;;
##############################################
hol88-2.02.19940316/Library/string/Manual/index.tex-2-
hol88-2.02.19940316/Library/string/Manual/index.tex:3: \item \verb+"`+$\dots$\verb+`"+ (string constants), 5--6
hol88-2.02.19940316/Library/string/Manual/index.tex-4- \item {\ptt ``\_DEF}, 14
##############################################
hol88-2.02.19940316/Library/string/Manual/string.idx-29-\indexentry{string constants|(}{5}
hol88-2.02.19940316/Library/string/Manual/string.idx:30:\indexentry{\\\@\verb+""`+$\dots$\verb+`""+ (string constants)|(}{5}
hol88-2.02.19940316/Library/string/Manual/string.idx-31-\indexentry{string\_CONV@{\ptt string\_CONV}|(}{5}
hol88-2.02.19940316/Library/string/Manual/string.idx-32-\indexentry{string constants|)}{6}
hol88-2.02.19940316/Library/string/Manual/string.idx:33:\indexentry{\\\@\verb+""`+$\dots$\verb+`""+ (string constants)|)}{6}
hol88-2.02.19940316/Library/string/Manual/string.idx-34-\indexentry{string\_CONV@{\ptt string\_CONV}|)}{6}
##############################################
hol88-2.02.19940316/Library/string/Manual/description.tex-269-\index{string constants|(}
hol88-2.02.19940316/Library/string/Manual/description.tex:270:\index{\\\@\verb+""`+$\dots$\verb+`""+ (string constants)|(}
hol88-2.02.19940316/Library/string/Manual/description.tex-271-
##############################################
hol88-2.02.19940316/Library/string/Manual/description.tex-350-\index{string constants|)}
hol88-2.02.19940316/Library/string/Manual/description.tex:351:\index{\\\@\verb+""`+$\dots$\verb+`""+ (string constants)|)}
hol88-2.02.19940316/Library/string/Manual/description.tex-352-\index{string\_CONV@{\ptt string\_CONV}|)}
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-198- list_mk_forall(getvs con,con) else
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:199: let asm = list_mk_conj (map mkp as) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:200: let pvs = getvs asm and cvs = getvs con in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-201- let qcon = list_mk_forall(subtract cvs pvs, con) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:202: let qasm = list_mk_exists(subtract pvs cvs, asm) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-203- let avs = intersect pvs cvs in
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-479- let bth = LIST_BETA_CONV red in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:480: let asm = list_mk_forall(vs,rand(rand(concl bth))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-481- let th1 = SPECL vs (ASSUME asm) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-482- let th2 = EQ_MP (SYM bth) (CONJ (SPECL vs ax) th1) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:483: DISCH asm (GENL vs th2);;
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-484-
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-485-% --------------------------------------------------------------------- %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:486:% INTERNAL FUNCION : reduce_asm %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-487-% %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:488:% The term asm is expected to be the antecedent of a rule in the form: %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-489-% %
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-496-% appear as conjuncts (possibly among some side conditions). The %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:497:% function reduce_asm beta-reduces these conjuncts and flattens the %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-498-% resulting conjunction of terms. The result is the theorem: %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-499-% %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:500:% |- asm ==> ?zs. ... /\ REL ps <args> /\ P <args> /\ ... %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-501-% %
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-503-
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:504:let reduce_asm =
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-505- letrec reduce fn tm =
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-509- let thm1 = CONJ t1 (CONJ t2 (UNDISCH imp)) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:510: let asm = mk_conj(c1,rand(rator(concl imp))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-511- let h1,h2 = CONJ_PAIR(ASSUME asm) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:512: DISCH asm (PROVE_HYP h1 (PROVE_HYP h2 thm1)) else
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-513- IMP_CONJ (DISCH c1 (ASSUME c1)) imp) ?
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-516- DISCH tm (ASSUME tm) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:517: \fn asm. let vs,body = strip_exists asm in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-518- itlist EXISTS_IMP vs (reduce fn body);;
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-520-% --------------------------------------------------------------------- %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:521:% INTERNAL FUNCTION : prove_asm %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-522-% %
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-526-% %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:527:% prove_asm filters out those conjuncts of the form "P <args>". The %
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-528-% theorem returned is: %
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-534-
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:535:let prove_asm P tm =
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-536- let test t = not(fst(strip_comb(concl t)) = P) in
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-562- let (cvs,a,c) = (I # dest_conj) (strip_forall cncl) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:563: let simpl = prove_asm (fst(strip_comb c)) ante in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-564- let thm1 = SPECL cvs (UNDISCH (IMP_TRANS simpl srul)) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:565: let newasm = list_mk_forall (vs, mk_imp(ante,list_mk_forall (cvs,c))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-566- let thm2 = CONJ thm1 (SPECL cvs (UNDISCH (SPECL vs (ASSUME newasm)))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:567: DISCH newasm (GENL vs (DISCH ante (GENL cvs thm2)));;
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-568-
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-595- let cvs,red = strip_forall c in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:596: let basm = reduce_asm (fst(strip_comb red)) a in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-597- let bth = itlist FORALL_EQ cvs (LIST_BETA_CONV red) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:598: let asm = list_mk_forall(vs,mk_imp (rand(concl basm),rand(concl bth))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:599: let thm1 = UNDISCH (IMP_TRANS basm (SPECL vs (ASSUME asm))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:600: let thm2 = DISCH asm (GENL vs (DISCH a (EQ_MP (SYM bth) thm1))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-601- let thm3 = simp_concl rul (rand(rator(concl thm2))) in
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-949- (let asm,cvs,cncl = (I # strip_forall) (dest_imp rule) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:950: let ith = DISCH asm (SPECL cvs (UNDISCH (SPECL vs th))) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-951- \(A,g).
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-1240- let th1 = EXISTS (mk_exists(x,cncl),x) (UNDISCH th) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:1241: let asm = mk_exists(x,ante) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:1242: DISCH asm (CHOOSE (x,ASSUME asm) th1) else
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:1243: let asm = mk_exists(x,ante) in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:1244: DISCH asm (CHOOSE (x,ASSUME asm) (UNDISCH th));;
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-1245-
##############################################
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-1260- let Q' = subst(combine(ys',ys)) Q in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:1261: let asm = CONJ (ASSUME P) (ASSUME Q') in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml:1262: let ths = CONJUNCTS asm in
hol88-2.02.19940316/Library/ind_defs/ind-defs.ml-1263- let realths = ths in
##############################################
hol88-2.02.19940316/Library/sets/gspec.ml-99- let r = lhs eq in
hol88-2.02.19940316/Library/sets/gspec.ml:100: let asm = subst [r,x] body in
hol88-2.02.19940316/Library/sets/gspec.ml:101: let imp2 = DISCH asm (EXISTS (tm,r) (CONJ (REFL r) (ASSUME asm))) in
hol88-2.02.19940316/Library/sets/gspec.ml-102- IMP_ANTISYM_RULE imp1 imp2;;
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-12- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile:13: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-14- 'compilet `term_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-19- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile:20: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-21- 'loadf `term_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-26- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile:27: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-28- 'loadf `term_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-35- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile:36: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-37- 'loadf `term_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-44- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile:45: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/HOL/Makefile-46- 'loadf `term_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml-31-
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml:32:let dummy() = preterm_var `$$FOO$$`
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml-33-and inner(op,T,ty1,ty2,ty3) =
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml-45- if can Dest_var T2 then
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml:46: if (Dest_var T2) = `$$FOO$$` then
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml-47- T1
##############################################
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml-51- if can Dest_var T2 then
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml:52: if (Dest_var T2) = `$$FOO$$` then
hol88-2.02.19940316/Library/parser/Examples/HOL/term_help.ml-53- T1
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-12- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:13: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-14- 'compilet `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-18- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:19: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-20- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-25- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:26: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-27- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-35- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:36: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-37- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-45- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:46: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-47- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-55- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:56: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-57- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-66- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:67: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-68- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-78- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:79: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-80- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-91- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:92: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-93- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-105- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:106: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-107- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-120- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:121: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-122- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-136- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:137: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-138- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-153- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:154: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-155- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-171- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:172: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-173- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-190- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:191: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-192- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-215- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:216: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-217- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-236- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:237: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-238- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-258- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:259: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-260- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-281- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:282: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-283- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-305- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:306: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-307- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-330- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:331: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-332- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-356- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:357: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-358- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-383- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:384: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-385- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-411- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:412: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-413- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-440- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:441: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-442- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-470- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile:471: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/ella/Makefile-472- 'loadf `PP_printer`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile-12- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile:13: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile-14- 'compilet `tiny_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile-19- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile:20: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile-21- 'loadf `tiny_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile-27- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile:28: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/tiny/Makefile-29- 'loadf `tiny_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/user_guide/blocks/Makefile-14- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/blocks/Makefile:15: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/blocks/Makefile-16- 'compilet `blocks_decls`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/user_guide/blocks/Makefile-21- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/blocks/Makefile:22: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/blocks/Makefile-23- 'loadf `blocks_decls`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/user_guide/bool/Makefile-14- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/bool/Makefile:15: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/bool/Makefile-16- 'compilet `bool_decls`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/user_guide/bool/Makefile-21- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/bool/Makefile:22: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/bool/Makefile-23- 'loadf `bool_decls`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile-12- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile:13: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile-14- 'compilet `types_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile-19- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile:20: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile-21- 'loadf `types_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile-27- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile:28: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Examples/user_guide/types/Makefile-29- 'loadf `types_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Manual/description.tex-213- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex:214: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex-215- 'compilet `bool_decls`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Manual/description.tex-220- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex:221: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex-222- 'loadf `bool_decls`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Manual/description.tex-849- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex:850: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex-851- 'compilet `types_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Manual/description.tex-856- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex:857: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex-858- 'loadf `types_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/Manual/description.tex-864- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex:865: 'loadf `$(GENERAL)`;;'\
hol88-2.02.19940316/Library/parser/Manual/description.tex-866- 'loadf `types_help`;;'\
##############################################
hol88-2.02.19940316/Library/parser/parser.ml-133- write_string ` echo 'set_flag(\`abort_when_fail\`,true);;'\\\L` outf;
hol88-2.02.19940316/Library/parser/parser.ml:134: write_string `\T 'loadf \`$(GENERAL)\`;;'\\\L` outf;
hol88-2.02.19940316/Library/parser/parser.ml-135- write_string (concatl [`\T 'compilet \``;filename;`_decls\`;;'\\\L`])
hol88-2.02.19940316/Library/parser/parser.ml-136- outf;
hol88-2.02.19940316/Library/parser/parser.ml:137: write_string `\T 'quit();;' | $(HOL)\L\L` outf;
hol88-2.02.19940316/Library/parser/parser.ml-138- write_string `# Finally do the actual functions\L` outf;
##############################################
hol88-2.02.19940316/Library/parser/parser.ml-140- write_string ` echo 'set_flag(\`abort_when_fail\`,true);;'\\\L` outf;
hol88-2.02.19940316/Library/parser/parser.ml:141: write_string `\T 'loadf \`$(GENERAL)\`;;'\\\L` outf;
hol88-2.02.19940316/Library/parser/parser.ml-142- write_string (concatl [`\T 'loadf \``;decs;`\`;;'\\\L`])
##############################################
hol88-2.02.19940316/Library/parser/parser.ml-144- write_string (concatl [`\T 'compilet \``;filename;`\`;;'\\\L`]) outf;
hol88-2.02.19940316/Library/parser/parser.ml:145: write_string ` 'quit();;' | $(HOL)\L\L` outf;
hol88-2.02.19940316/Library/parser/parser.ml-146- write_string (concatl [`all: `;file;`_ml.o\L`]) outf;
##############################################
hol88-2.02.19940316/Library/pred_sets/gspec.ml-99- let r = lhs eq in
hol88-2.02.19940316/Library/pred_sets/gspec.ml:100: let asm = subst [r,x] body in
hol88-2.02.19940316/Library/pred_sets/gspec.ml:101: let imp2 = DISCH asm (EXISTS (tm,r) (CONJ (REFL r) (ASSUME asm))) in
hol88-2.02.19940316/Library/pred_sets/gspec.ml-102- IMP_ANTISYM_RULE imp1 imp2;;
##############################################
hol88-2.02.19940316/Library/more_arithmetic/tools.ml-425- let ([asm], asl') = take_first is_exists asl in
hol88-2.02.19940316/Library/more_arithmetic/tools.ml:426: let (x,A) = dest_exists asm in
hol88-2.02.19940316/Library/more_arithmetic/tools.ml-427- let x' = variant (terml_frees(C.asl)) x in
##############################################
hol88-2.02.19940316/Library/window/inter.ml-175- else if (term_mem h usedcnjs) then
hol88-2.02.19940316/Library/window/inter.ml:176: print_string ` $ `
hol88-2.02.19940316/Library/window/inter.ml-177- else if (term_mem h hyps) then
##############################################
hol88-2.02.19940316/Library/window/window.ml-83-let window_version =
hol88-2.02.19940316/Library/window/window.ml:84: implode (rev (tl (tl (rev (tl (explode `$Revision: 3.1 $`))))));;
hol88-2.02.19940316/Library/window/window.ml-85-
##############################################
hol88-2.02.19940316/Library/abs_theory/Makefile-71- 'set_search_path (search_path() @ '\
hol88-2.02.19940316/Library/abs_theory/Makefile:72: ' [`${Root}/ml/`;'\
hol88-2.02.19940316/Library/abs_theory/Makefile-73- ' ]);;'\
hol88-2.02.19940316/Library/abs_theory/Makefile:74: 'loadt `${Home}/$*.ml`;;'\
hol88-2.02.19940316/Library/abs_theory/Makefile-75- 'quit();;' | ${Hol} || ${RM} $*.th
##############################################
hol88-2.02.19940316/Library/abs_theory/Makefile-93- 'set_search_path (search_path() @ '\
hol88-2.02.19940316/Library/abs_theory/Makefile:94: ' [`${Root}/ml/`;'\
hol88-2.02.19940316/Library/abs_theory/Makefile-95- ' ]);;'\
##############################################
hol88-2.02.19940316/Library/pair/both2.ml-245- let th1 = PEXISTS (mk_pexists(p,c),p) (UNDISCH th) in
hol88-2.02.19940316/Library/pair/both2.ml:246: let asm = mk_pexists(p,a) in
hol88-2.02.19940316/Library/pair/both2.ml:247: let th2 = DISCH asm (PCHOOSE (p, ASSUME asm) th1) in
hol88-2.02.19940316/Library/pair/both2.ml-248- (CONV_RULE (RAND_CONV (GEN_PALPHA_CONV p))) th2
##############################################
hol88-2.02.19940316/Library/pair/conv.ml-835- let tm = mk_forall(x, mk_imp (P, Q)) in
hol88-2.02.19940316/Library/pair/conv.ml:836: let asm = mk_exists(x,P) in
hol88-2.02.19940316/Library/pair/conv.ml-837- let th1 = GEN x (CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm)))) in
hol88-2.02.19940316/Library/pair/conv.ml:838: let imp1 = DISCH tm (DISCH asm th1) in
hol88-2.02.19940316/Library/pair/conv.ml-839- let cncl = rand(concl imp1) in
##############################################
hol88-2.02.19940316/Library/pair/conv.ml-853- let tm = mk_forall(x, mk_imp (P, Q)) in
hol88-2.02.19940316/Library/pair/conv.ml:854: let asm = mk_exists(x,P) in
hol88-2.02.19940316/Library/pair/conv.ml-855- let th1 = CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm))) in
hol88-2.02.19940316/Library/pair/conv.ml:856: let imp1 = DISCH tm (DISCH asm th1) in
hol88-2.02.19940316/Library/pair/conv.ml-857- let cncl = rand(concl imp1) in
##############################################
hol88-2.02.19940316/Library/pair/pair.ml-58-let pair_version =
hol88-2.02.19940316/Library/pair/pair.ml:59: implode (rev (tl (tl (rev (tl (explode `$Revision: 3.1 $`))))));;
hol88-2.02.19940316/Library/pair/pair.ml-60-
##############################################
hol88-2.02.19940316/Library/res_quan/Manual/entries.tex-368-\begin{verbatim}
hol88-2.02.19940316/Library/res_quan/Manual/entries.tex:369: asm ?- Pk' ... asm ?- Pm' {asm,Pk',...,Pm'} ?- gl'
hol88-2.02.19940316/Library/res_quan/Manual/entries.tex-370-\end{verbatim}
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-18- | (asm.asml) .
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:19: let ml = match_aa ante asm in
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-20- (if (match_ok (intersect fvars (frees ante)) ml)
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-26-
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:27:letrec match_asm fvars asm (ml,pl) =
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-28- fun [] . (ml,pl)
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-29- | (ante. antes) .
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:30: let mlist = match_aal fvars ante asm in
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-31- if null mlist then % no match %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:32: (match_asm fvars asm (ml,pl) antes)
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-33- else (let ml' = fst (hd mlist) in
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-35- then % found consistant match %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:36: (match_asm fvars asm (ml', (ante.pl)) antes)
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-37- else if (subset ml' ml)
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-38- then % found consistant match %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:39: (match_asm fvars asm (ml, (ante.pl)) antes)
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-40- else % inconsistant match %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:41: (match_asm fvars asm (ml, pl) antes)) ;;
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-42-
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-46-% -> term list -> (term list # thm) %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:47:% MATCH_SUBS1 th m1 asm fvs = [tm1;...], th' %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-48-% INPUTS: %
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-50-% m1 is a list indicating an instantiation of th. %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:51:% asm is a list of terms from which instances of the antecedents of th %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-52-% are found. %
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-56-% tmi's are instances of the antecedents of th which do not appear in %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:57:% the assumptions asm %
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-58-% th' is an instance of th resulting from substituting the matches in %
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-73-
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:74:let MATCH_SUBS1 th fvs asm m1 =
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-75- let afilter l fvs =
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-88- else
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:89: (let rlist = match_asm nv asm ([],[])
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-90- (afilter (combine(antes, antes')) nv) in
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-95-
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:96:let MATCH_SUBS th fvs asm mlist =
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-97- let mll = map (MATCH_SUBS1 th fvs asm) mlist in
##############################################
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-132- let mlist = fn tml gl in
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml:133: let sgl,thms = (MATCH_SUBS th freevars asm mlist) in
hol88-2.02.19940316/Library/res_quan/cond_rewr.ml-134- if null mlist then failwith `no match`
##############################################
hol88-2.02.19940316/Library/res_quan/help/entries/COND_REWR_TAC.doc-75-{
hol88-2.02.19940316/Library/res_quan/help/entries/COND_REWR_TAC.doc:76: asm ?- Pk' ... asm ?- Pm' {{asm,Pk',...,Pm'}} ?- gl'
hol88-2.02.19940316/Library/res_quan/help/entries/COND_REWR_TAC.doc-77-}
##############################################
hol88-2.02.19940316/Library/word/Manual/model_word.tex-624-\]
hol88-2.02.19940316/Library/word/Manual/model_word.tex:625:where $k = k_1 + k_2$ and $n$, $k_1$, $k_2$, $m_1$ and $m_2$ are
hol88-2.02.19940316/Library/word/Manual/model_word.tex-626-numeric constants and satisfy the following relations: $k_1 + m_1\leq
##############################################
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2-25- do map create_doc_file (thl@axl@del) in
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2:26: let ok = (new_theory \`dummy$$\`; new_parent \`$1\`; true) ? false in
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2-27- print_string \`!!\`; print_newline();
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2:28: ok => create_doc_files \`$1\` | print_string \`echo Failed\`;
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2-29- print_newline(); print_string \`??\`; print_newline();
##############################################
hol88-2.02.19940316/Library/word/help/thms/word_base/create-doc-files2-26- do map create_doc_file (thl@axl@del) in
hol88-2.02.19940316/Library/word/help/thms/word_base/create-doc-files2:27: let ok = (new_theory \`dummy$$\`; new_parent \`$1\`; true) ? false in
hol88-2.02.19940316/Library/word/help/thms/word_base/create-doc-files2-28- print_string \`!!\`; print_newline();
hol88-2.02.19940316/Library/word/help/thms/word_base/create-doc-files2:29: ok => create_doc_files \`$1\` | print_string \`echo Failed\`;
hol88-2.02.19940316/Library/word/help/thms/word_base/create-doc-files2-30- print_newline(); print_string \`??\`; print_newline();
##############################################
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2~-27- do map create_doc_file (thl@axl@del) in
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2~:28: let ok = (new_theory \`dummy$$\`; new_parent \`$1\`; true) ? false in
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2~-29- print_string \`!!\`; print_newline();
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2~:30: ok => create_doc_files \`$1\` | print_string \`echo Failed\`;
hol88-2.02.19940316/Library/word/help/thms/create-doc-files2~-31- print_newline(); print_string \`??\`; print_newline();
##############################################
hol88-2.02.19940316/Library/record_proof/proof_rec.ml-760-let sanitise str =
hol88-2.02.19940316/Library/record_proof/proof_rec.ml:761: let sps = explode `.;,:"!@#$^&*()|\\` in
hol88-2.02.19940316/Library/record_proof/proof_rec.ml-762- let c' = `_` in
##############################################
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-17- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile:18: 'load_library`$(LIB)`;;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-19- 'loadt `HOL_MULT`;;'\
##############################################
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-23- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile:24: 'load_library`$(LIB)`;;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-25- 'loadt `MULT_FUN`;;'\
##############################################
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-29- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile:30: 'load_library`$(LIB)`;;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-31- 'loadt `MULT_FUN_CURRY`;;'\
##############################################
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-35- echo 'set_flag(`abort_when_fail`,true);;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile:36: 'load_library`$(LIB)`;;'\
hol88-2.02.19940316/Library/record_proof/benchmark/Makefile-37- 'loadt `mk_NEXT`;;'\
##############################################
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-527- CONJ_PAIR (REWRITE_RULE [is_basen_both] is_basen_cons) in
hol88-2.02.19940316/Library/numeral/numeral_theory.ml:528: let tail_less = MP (MP asm less_radix) is_basen in
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-529- ASSUME_TAC tail_less THEN
##############################################
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-620- IMP_RES_TAC IS_BASEN_CONS_IMP_IS_BASEN THEN
hol88-2.02.19940316/Library/numeral/numeral_theory.ml:621: let induction_asm =
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-622- ASSUME "!l2 r. 1 < r ==> IS_BASEN r l1 ==> IS_BASEN r l2 ==>
##############################################
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-929- ASM_REWRITE_TAC [LENGTH; BASEN; INV_SUC_EQ] THEN
hol88-2.02.19940316/Library/numeral/numeral_theory.ml:930: let induct_asm =
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-931- ASSUME "!n r.
##############################################
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-938- (SPECL ["n MOD (r EXP m)"; "r: num"])
hol88-2.02.19940316/Library/numeral/numeral_theory.ml:939: ) induct_asm in
hol88-2.02.19940316/Library/numeral/numeral_theory.ml-940- let [exists_lemma1; exists_lemma2] =
##############################################
hol88-2.02.19940316/Versions/Version.1.12-2624-DEPTH_FORALL_CONV OR_IMP mk_injs
hol88-2.02.19940316/Versions/Version.1.12:2625:DO_ASM PROJ mk_new_vars
hol88-2.02.19940316/Versions/Version.1.12-2626-ELIM_ANTE_EQNS_CONV RM_LEN_CONV mk_subset_pred
##############################################
hol88-2.02.19940316/contrib/Xhelp/hol_apro.orig-5-DEFHOLHELPPATH=ORIG_HELP_PATH/ENTRIES
hol88-2.02.19940316/contrib/Xhelp/hol_apro.orig:6:CUR_HELP_PATH=`echo ${HOL_HELP_PATH} ${DEFHOLHELPPATH} |sed 's/ /:/g'`
hol88-2.02.19940316/contrib/Xhelp/hol_apro.orig-7-
##############################################
hol88-2.02.19940316/contrib/Xhelp/hol_ref.orig-5-DEFHOLHELPPATH=ORIG_HELP_PATH/ENTRIES
hol88-2.02.19940316/contrib/Xhelp/hol_ref.orig:6:CUR_HELP_PATH=`echo ${HOL_HELP_PATH} ${DEFHOLHELPPATH} |sed 's/ /:/g'`
hol88-2.02.19940316/contrib/Xhelp/hol_ref.orig-7-
##############################################
hol88-2.02.19940316/contrib/Xhelp/hol_thm.orig-5-DEFTHMHELPPATH=ORIG_HELP_PATH/THEOREMS/*
hol88-2.02.19940316/contrib/Xhelp/hol_thm.orig:6:CUR_HELP_PATH=`echo ${THM_HELP_PATH} ${DEFTHMHELPPATH} |sed 's/ /:/g'`
hol88-2.02.19940316/contrib/Xhelp/hol_thm.orig-7-
##############################################
hol88-2.02.19940316/contrib/Xhelp/hol_apro-5-DEFHOLHELPPATH=/usr/groups/hol/HOL21/src/help/ENTRIES
hol88-2.02.19940316/contrib/Xhelp/hol_apro:6:CUR_HELP_PATH=`echo ${HOL_HELP_PATH} ${DEFHOLHELPPATH} |sed 's/ /:/g'`
hol88-2.02.19940316/contrib/Xhelp/hol_apro-7-
##############################################
hol88-2.02.19940316/contrib/Xhelp/hol_ref-5-DEFHOLHELPPATH=/usr/groups/hol/HOL21/src/help/ENTRIES
hol88-2.02.19940316/contrib/Xhelp/hol_ref:6:CUR_HELP_PATH=`echo ${HOL_HELP_PATH} ${DEFHOLHELPPATH} |sed 's/ /:/g'`
hol88-2.02.19940316/contrib/Xhelp/hol_ref-7-
##############################################
hol88-2.02.19940316/contrib/Xhelp/hol_thm-5-DEFTHMHELPPATH=/usr/groups/hol/HOL21/src/help/THEOREMS/*
hol88-2.02.19940316/contrib/Xhelp/hol_thm:6:CUR_HELP_PATH=`echo ${THM_HELP_PATH} ${DEFTHMHELPPATH} |sed 's/ /:/g'`
hol88-2.02.19940316/contrib/Xhelp/hol_thm-7-
##############################################
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml-179- let imp1 = DISCH tm (SUBST[thm1,v] P thm2) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml:180: let asm = subst[r,l] P in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml:181: let imp2 = DISCH asm (EXISTS (tm,r) (CONJ (REFL r) (ASSUME asm))) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml-182- IMP_ANTISYM_RULE imp1 imp2
##############################################
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml-191- let imp1 = DISCH tm (SUBST[thm2,v] P thm1) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml:192: let asm = subst[r,l] P in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml:193: let imp2 = DISCH asm (EXISTS (tm,r) (CONJ (ASSUME asm) (REFL r))) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml-194- IMP_ANTISYM_RULE imp1 imp2
##############################################
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml-201- let imp1 = DISCH tm (MP (SPEC r (ASSUME tm)) (REFL r)) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml:202: let asm = rand(concl imp1) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml-203- let th1 = SUBST [SYM(ASSUME eq),v] P (ASSUME asm) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml:204: let imp2 = DISCH asm (GEN v (DISCH eq th1)) in
hol88-2.02.19940316/contrib/RefCalc/defs/defs.ml-205- IMP_ANTISYM_RULE imp1 imp2
##############################################
hol88-2.02.19940316/contrib/tex-thy-format/format_thy-1-echo 'loadf`format_thy`;; '\
hol88-2.02.19940316/contrib/tex-thy-format/format_thy:2: 'load_theory`'$1'`;; '\
hol88-2.02.19940316/contrib/tex-thy-format/format_thy:3: 'format_theory`'$1'`;; '\
hol88-2.02.19940316/contrib/tex-thy-format/format_thy-4- 'quit();;' |hol |\
##############################################
hol88-2.02.19940316/contrib/mut_rec_types/mut_def.ml-23-%%
hol88-2.02.19940316/contrib/mut_rec_types/mut_def.ml:24:let sum_type_name = `SUM_OF` ^ (foldl1 $^ (map ($^ `_`) names)) in
hol88-2.02.19940316/contrib/mut_rec_types/mut_def.ml-25-
##############################################
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-86-% Complicated... used in LEN_SIMP_CONV below... %
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml:87:letrec DO_ASM th asm =
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-88- if (not(is_exists (concl asm))) then
##############################################
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-98- let (v,body) = dest_exists (concl asm) in
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml:99: let thm1 = DO_ASM th (ASSUME body) in CHOOSE (v,asm)thm1;;
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-100-
##############################################
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-108- let res = snd(dest_imp(concl imp1)) in
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml:109: let asm = ASSUME res in
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-110- let th4 = REFL (rand(rhs(snd(strip_exists res)))) in
##############################################
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-112- let th5 = EXISTS_RULE evars th4 in
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml:113: let imp2 = DISCH res (DO_ASM th5 asm) in
hol88-2.02.19940316/contrib/SECD/wordn/wordn.ml-114- IMP_ANTISYM_RULE imp1 imp2;;
##############################################
hol88-2.02.19940316/contrib/SECD/SECD_proofs.ml-83-% right away for their use later: %
hol88-2.02.19940316/contrib/SECD/SECD_proofs.ml:84:% - DP_lemma puts the Clock_constraint" on the asm list. %
hol88-2.02.19940316/contrib/SECD/SECD_proofs.ml-85-% - one_asserted_lemma is specialized for substitution. %
##############################################
hol88-2.02.19940316/contrib/SECD/SECD_proofs.ml-251- THEN port[PF_lemma] % set up to remove quantified vars %
hol88-2.02.19940316/contrib/SECD/SECD_proofs.ml:252: THEN STRIP_TAC % constraint on asm list for lemma %
hol88-2.02.19940316/contrib/SECD/SECD_proofs.ml-253- THEN port[lemma] % eliminate one-assertedness %
##############################################
hol88-2.02.19940316/contrib/SECD/correctness_misc.ml-476-% - Strip off nonintersecting assumption, GENeralize "cell", %
hol88-2.02.19940316/contrib/SECD/correctness_misc.ml:477:% RESOLVE nonintersecting_free_1_lemma with asm list %
hol88-2.02.19940316/contrib/SECD/correctness_misc.ml-478-% and this asm., then SPECialize to the null list, getting the %
##############################################
hol88-2.02.19940316/contrib/SECD/correctness_misc.ml-487-% - Substitute the "T" assumption in the ind. assum. and also %
hol88-2.02.19940316/contrib/SECD/correctness_misc.ml:488:% resolve with the asm from nonintersecting_car_cdr_lemma. %
hol88-2.02.19940316/contrib/SECD/correctness_misc.ml-489-% - Do the COND_CASES on the head of the path list ("h"), %
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_LD2.ml-452-let state_prover test_lemma thm =
hol88-2.02.19940316/contrib/SECD/mu-prog_LD2.ml:453:let asm = (mk_comb
hol88-2.02.19940316/contrib/SECD/mu-prog_LD2.ml-454- o ((\th. (mk_comb ("$=:num->num->bool", (snd o dest_comb) th))) # I)
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_LD2.ml-479-let nonmajor_prover thm =
hol88-2.02.19940316/contrib/SECD/mu-prog_LD2.ml:480:let asm = (mk_comb
hol88-2.02.19940316/contrib/SECD/mu-prog_LD2.ml-481- o ((\th. (mk_comb ("$=:num->num->bool", (snd o dest_comb) th))) # I)
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_init_proofs.ml-94-let prove_jump_steps (n, stem) =
hol88-2.02.19940316/contrib/SECD/mu-prog_init_proofs.ml:95: let asm =
hol88-2.02.19940316/contrib/SECD/mu-prog_init_proofs.ml-96- mk_eq ("opcode_bits(memory (t:^mtime)(car_bits(memory t(c t))))",
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_init_proofs.ml-99- let th1,th2 = prove_next_step ptheory
hol88-2.02.19940316/contrib/SECD/mu-prog_init_proofs.ml:100: (SUBS [ASSUME asm] l1, ADD_ASSUM asm l2)
hol88-2.02.19940316/contrib/SECD/mu-prog_init_proofs.ml-101- in
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml-263-% ================================================================= %
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml:264:let prove_next_interval asm ((th1a,th1b),(th2a,th2b)) =
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml-265- let mpc_t = CONJUNCT1 th1a
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml-303-% ================================================================= %
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml:304:let asm = "(free(PRE t) = NIL_addr) = F";;
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml-305-
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml-322-`)
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml:323: ; recursive f (prove_next_interval asm (arg, thms))))
hol88-2.02.19940316/contrib/SECD/mu-prog_proof_fcn.ml-324- | (in_major_state nextA) % else if major state reached %
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml-265-% ================================================================= %
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml:266:let prove_next_interval asm ((th1a,th1b),(th2a,th2b)) =
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml-267- let mpc_t = CONJUNCT1 th1a
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml-308-% ================================================================= %
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml:309:let asm = "(free(PRE t) = NIL_addr) = F";;
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml-310-let ptheory = `phase_lemmas7`;;
##############################################
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml-328- in
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml:329: recursive f (prove_next_interval asm (arg, thms)))
hol88-2.02.19940316/contrib/SECD/mu-prog_sr_proofs.ml-330- | recursive f (f arg)
##############################################
hol88-2.02.19940316/contrib/SECD/Makefile-102-.ml.th:; /bin/rm -f $*.th $*.log
hol88-2.02.19940316/contrib/SECD/Makefile:103: echo 'loadt `$*`;;'\
hol88-2.02.19940316/contrib/SECD/Makefile-104- 'quit();;' | ${Hol} > $*.log 2>&1
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-18- | (asm.asml) .
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:19: let ml = match_aa ante asm in
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-20- (if (match_ok (intersect fvars (frees ante)) ml)
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-26-
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:27:letrec match_asm fvars asm (ml,pl) =
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-28- fun [] . (ml,pl)
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-29- | (ante. antes) .
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:30: let mlist = match_aal fvars ante asm in
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-31- if null mlist then % no match %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:32: (match_asm fvars asm (ml,pl) antes)
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-33- else (let ml' = fst (hd mlist) in
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-35- then % found consistant match %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:36: (match_asm fvars asm (ml', (ante.pl)) antes)
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-37- else if (subset ml' ml)
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-38- then % found consistant match %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:39: (match_asm fvars asm (ml, (ante.pl)) antes)
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-40- else % inconsistant match %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:41: (match_asm fvars asm (ml, pl) antes)) ;;
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-42-
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-46-% -> term list -> (term list # thm) %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:47:% MATCH_SUBS1 th m1 asm fvs = [tm1;...], th' %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-48-% INPUTS: %
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-50-% m1 is a list indicating an instantiation of th. %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:51:% asm is a list of terms from which instances of the antecedents of th %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-52-% are found. %
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-56-% tmi's are instances of the antecedents of th which do not appear in %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:57:% the assumptions asm %
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-58-% th' is an instance of th resulting from substituting the matches in %
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-73-
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:74:let MATCH_SUBS1 th fvs asm m1 =
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-75- let afilter l fvs =
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-88- else
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:89: (let rlist = match_asm nv asm ([],[])
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-90- (afilter (combine(antes, antes')) nv) in
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-95-
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:96:let MATCH_SUBS th fvs asm mlist =
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-97- let mll = map (MATCH_SUBS1 th fvs asm) mlist in
##############################################
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-132- let mlist = fn tml gl in
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml:133: let sgl,thms = (MATCH_SUBS th freevars asm mlist) in
hol88-2.02.19940316/contrib/res_quan/cond_rewr.ml-134- if null mlist then failwith `no match`
##############################################
hol88-2.02.19940316/contrib/newrw/newrw-30-
hol88-2.02.19940316/contrib/newrw/newrw:31:if test `/usr/bin/fgrep $TARGET $FILE | /usr/ucb/wc -l` -eq 0
hol88-2.02.19940316/contrib/newrw/newrw-32-then
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-198- list_mk_forall(getvs con,con) else
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:199: let asm = list_mk_conj (map mkp as) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:200: let pvs = getvs asm and cvs = getvs con in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-201- let qcon = list_mk_forall(subtract cvs pvs, con) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:202: let qasm = list_mk_exists(subtract pvs cvs, asm) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-203- let avs = intersect pvs cvs in
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-479- let bth = LIST_BETA_CONV red in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:480: let asm = list_mk_forall(vs,rand(rand(concl bth))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-481- let th1 = SPECL vs (ASSUME asm) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-482- let th2 = EQ_MP (SYM bth) (CONJ (SPECL vs ax) th1) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:483: DISCH asm (GENL vs th2);;
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-484-
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-485-% --------------------------------------------------------------------- %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:486:% INTERNAL FUNCION : reduce_asm %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-487-% %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:488:% The term asm is expected to be the antecedent of a rule in the form: %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-489-% %
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-496-% appear as conjuncts (possibly among some side conditions). The %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:497:% function reduce_asm beta-reduces these conjuncts and flattens the %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-498-% resulting conjunction of terms. The result is the theorem: %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-499-% %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:500:% |- asm ==> ?zs. ... /\ REL ps <args> /\ P <args> /\ ... %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-501-% %
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-503-
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:504:let reduce_asm =
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-505- letrec reduce fn tm =
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-509- let thm1 = CONJ t1 (CONJ t2 (UNDISCH imp)) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:510: let asm = mk_conj(c1,rand(rator(concl imp))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-511- let h1,h2 = CONJ_PAIR(ASSUME asm) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:512: DISCH asm (PROVE_HYP h1 (PROVE_HYP h2 thm1)) else
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-513- IMP_CONJ (DISCH c1 (ASSUME c1)) imp) ?
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-516- DISCH tm (ASSUME tm) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:517: \fn asm. let vs,body = strip_exists asm in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-518- itlist EXISTS_IMP vs (reduce fn body);;
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-520-% --------------------------------------------------------------------- %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:521:% INTERNAL FUNCTION : prove_asm %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-522-% %
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-526-% %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:527:% prove_asm filters out those conjuncts of the form "P <args>". The %
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-528-% theorem returned is: %
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-534-
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:535:let prove_asm P tm =
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-536- let test t = not(fst(strip_comb(concl t)) = P) in
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-562- let (cvs,a,c) = (I # dest_conj) (strip_forall cncl) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:563: let simpl = prove_asm (fst(strip_comb c)) ante in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-564- let thm1 = SPECL cvs (UNDISCH (IMP_TRANS simpl srul)) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:565: let newasm = list_mk_forall (vs, mk_imp(ante,list_mk_forall (cvs,c))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-566- let thm2 = CONJ thm1 (SPECL cvs (UNDISCH (SPECL vs (ASSUME newasm)))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:567: DISCH newasm (GENL vs (DISCH ante (GENL cvs thm2)));;
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-568-
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-595- let cvs,red = strip_forall c in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:596: let basm = reduce_asm (fst(strip_comb red)) a in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-597- let bth = itlist FORALL_EQ cvs (LIST_BETA_CONV red) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:598: let asm = list_mk_forall(vs,mk_imp (rand(concl basm),rand(concl bth))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:599: let thm1 = UNDISCH (IMP_TRANS basm (SPECL vs (ASSUME asm))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:600: let thm2 = DISCH asm (GENL vs (DISCH a (EQ_MP (SYM bth) thm1))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-601- let thm3 = simp_concl rul (rand(rator(concl thm2))) in
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-949- (let asm,cvs,cncl = (I # strip_forall) (dest_imp rule) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:950: let ith = DISCH asm (SPECL cvs (UNDISCH (SPECL vs th))) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-951- \(A,g).
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-1226- let th1 = EXISTS (mk_exists(x,cncl),x) (UNDISCH th) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:1227: let asm = mk_exists(x,ante) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:1228: DISCH asm (CHOOSE (x,ASSUME asm) th1) else
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:1229: let asm = mk_exists(x,ante) in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:1230: DISCH asm (CHOOSE (x,ASSUME asm) (UNDISCH th));;
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-1231-
##############################################
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-1246- let Q' = subst(combine(ys',ys)) Q in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:1247: let asm = CONJ (ASSUME P) (ASSUME Q') in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml:1248: let ths = CONJUNCTS asm in
hol88-2.02.19940316/contrib/rule-induction/ind-defs.ml-1249- let realths = ths in
##############################################
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml-99- let w' = variant [w] w and W,B = dest_comb WB in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml:100: let asm = AP_TERM W (ASSUME (mk_eq(B,mk_comb(rator B,w')))) in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml:101: let thm = EQ_MP (MKEQ eq (SPEC w WBth)(SPEC w' WBth)) asm in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml-102- GEN w' (GEN w (DISCH (mk_eq(B,mk_comb(rator B,w'))) thm)))
##############################################
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml-123- let pat = mk_exists(w,mk_eq(mk_comb(rator(lhs BW),w),l)) in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml:124: let asm = EQ_MP (SPEC l BWth) (ASSUME len) in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml-125- GEN l (DISCH len (EXISTS(pat,rand(lhs BW)) asm))
##############################################
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml-151- let BITS,WORD = (I # rator) (dest_comb(lhs eq)) in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml:152: let asm = mk_eq(mk_comb(WORD,l),mk_comb(WORD,l')) in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml:153: let th1 = DISCH asm (EQ_MP thm (AP_TERM BITS (ASSUME asm))) in
hol88-2.02.19940316/contrib/wordn/wordn_rules.ml-154- GEN l (GEN l' (DISCH conj th1)))
##############################################
hol88-2.02.19940316/contrib/wordn/wordn_pack.ml-47- (define_bit_op defthm (`NOT`^nstr^`_DEF`) (`NOT`^nstr) "$~") .
hol88-2.02.19940316/contrib/wordn/wordn_pack.ml:48: (map def_binop [(`AND`,"$/\"); (`OR`,"$\/");
hol88-2.02.19940316/contrib/wordn/wordn_pack.ml-49- (`XOR`, "(\(x:bool) x'. ~(x=x'))")])
##############################################
hol88-2.02.19940316/contrib/aci/aci.ml-107-" , (
hol88-2.02.19940316/contrib/aci/aci.ml:108: DISCH_THEN \ ACI_REL_asm .
hol88-2.02.19940316/contrib/aci/aci.ml-109- REPEAT GEN_TAC THEN
hol88-2.02.19940316/contrib/aci/aci.ml:110: DISCH_THEN \ ASSOC_COMM_ID_asm .
hol88-2.02.19940316/contrib/aci/aci.ml-111- let [_; _; ID_asm] =
##############################################
hol88-2.02.19940316/contrib/aci/aci.ml-139-" , (
hol88-2.02.19940316/contrib/aci/aci.ml:140: DISCH_THEN \ ACI_REL_asm .
hol88-2.02.19940316/contrib/aci/aci.ml-141- REPEAT GEN_TAC THEN
hol88-2.02.19940316/contrib/aci/aci.ml:142: DISCH_THEN \ ASSOC_COMM_ID_asm .
hol88-2.02.19940316/contrib/aci/aci.ml-143- let [ASSOC_asm; COMM_asm; ID_asm] =
##############################################
hol88-2.02.19940316/contrib/aci/aci.ml-365- REPEAT GEN_TAC THEN
hol88-2.02.19940316/contrib/aci/aci.ml:366: DISCH_THEN \ ASSOC_COMM_ID_asm .
hol88-2.02.19940316/contrib/aci/aci.ml-367- let [ASSOC_asm; COMM_asm; _] =
##############################################
hol88-2.02.19940316/contrib/aci/aci.ml-378- in
hol88-2.02.19940316/contrib/aci/aci.ml:379: let ACI_OP_asm = MATCH_MP ACI_OP_DEF ASSOC_COMM_ID_asm
hol88-2.02.19940316/contrib/aci/aci.ml-380- in
##############################################
hol88-2.02.19940316/contrib/fpf/SSMART_EXISTS_TAC.ml-36-
hol88-2.02.19940316/contrib/fpf/SSMART_EXISTS_TAC.ml:37: let search_asm (chooseables,t,existentials,quant) asm = (
hol88-2.02.19940316/contrib/fpf/SSMART_EXISTS_TAC.ml-38- if (type_of t = ":bool") then (
##############################################
hol88-2.02.19940316/contrib/fpf/SSMART_EXISTS_TAC.ml-45- letrec bindings (chooseables,t,existentials,chex,quant) asms = (
hol88-2.02.19940316/contrib/fpf/SSMART_EXISTS_TAC.ml:46: let asm_bindings = flat (map (search_asm (chooseables,t,existentials,quant)) asms) in
hol88-2.02.19940316/contrib/fpf/SSMART_EXISTS_TAC.ml-47- let (sub_term_bindings,sub_asm_bindings) = (
##############################################
hol88-2.02.19940316/contrib/fpf/Makefile.fragments-18- echo 'letref retry = false;;' \
hol88-2.02.19940316/contrib/fpf/Makefile.fragments:19: '(compilet `$*`;'\
hol88-2.02.19940316/contrib/fpf/Makefile.fragments-20- 'quit());;' | ${Hol}
##############################################
hol88-2.02.19940316/contrib/fpf/Makefile.fragments-23- rm -f $*.th
hol88-2.02.19940316/contrib/fpf/Makefile.fragments:24: echo 'letref retry = false;; (loadt `$*`; quit());;' | ${Hol}
hol88-2.02.19940316/contrib/fpf/Makefile.fragments-25-
##############################################
hol88-2.02.19940316/contrib/smarttacs/SSMART_EXISTS_TAC.ml-36-
hol88-2.02.19940316/contrib/smarttacs/SSMART_EXISTS_TAC.ml:37: let search_asm (chooseables,t,existentials,quant) asm = (
hol88-2.02.19940316/contrib/smarttacs/SSMART_EXISTS_TAC.ml-38- if (type_of t = ":bool") then (
##############################################
hol88-2.02.19940316/contrib/smarttacs/SSMART_EXISTS_TAC.ml-45- letrec bindings (chooseables,t,existentials,chex,quant) asms = (
hol88-2.02.19940316/contrib/smarttacs/SSMART_EXISTS_TAC.ml:46: let asm_bindings = flat (map (search_asm (chooseables,t,existentials,quant)) asms) in
hol88-2.02.19940316/contrib/smarttacs/SSMART_EXISTS_TAC.ml-47- let (sub_term_bindings,sub_asm_bindings) = (
##############################################
hol88-2.02.19940316/contrib/smarttacs/SET_PROOFS.ml-36- else
hol88-2.02.19940316/contrib/smarttacs/SET_PROOFS.ml:37: let neq_asm = end_itlist (curry mk_conj) (map (\t. "~(^var = ^t)") inserts) in
hol88-2.02.19940316/contrib/smarttacs/SET_PROOFS.ml:38: PROVE("!^var. ^neq_asm ==> ~(^var IN ^s)",
hol88-2.02.19940316/contrib/smarttacs/SET_PROOFS.ml-39- GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [IN_INSERT;NOT_IN_EMPTY])
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-521- THEN ASM_REWRITE_TAC[]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:522: THEN REWRITE_ASM [TERM]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-523- THEN IMP_RES_TAC is_WHOLE_PR
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-577- THEN IMP_RES_TAC join_TERM
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:578: THEN REWRITE_ASM [TERM]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-579- THEN SUPPOSE_TAC "WHOLE 0 <+ WHOLE 1"
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-680- THEN RES_TAC
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:681: THEN REWRITE_ASM []
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-682- THEN ASM_REWRITE_TAC[]
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-953- THEN EXISTS_TAC "i:num"
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:954: THEN REWRITE_ASM [lengths]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:955: THEN CONV_ASM (DEPTH_CONV BETA_CONV)
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-956- THEN ASM_REWRITE_TAC[]
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1247- THEN IMP_RES_TAC exseq_subseq_length
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:1248: THEN REWRITE_ASM [exseq_subseq;lnum_less_eq_as_less]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1249- THEN FIRST_ASSUM DISJ_CASES_TAC
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1363- THEN ASM_REWRITE_TAC[PR_fn]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:1364: THEN REWRITE_ASM [TERM]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1365- THEN ASSUME_TAC (SPEC "e:exseq" length_min)
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1403- (REWRITE_RULE [trans] lnum_less_eq_trans)
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:1404: THEN REWRITE_ASM [PR]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1405- THEN IMP_RES_TAC lnum_strict_sub_mono_alt
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1450- THEN IMP_RES_TAC lnum_PR_mono_strict
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:1451: THEN REWRITE_ASM [PR;TERM]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1452- THEN UNDISCH_ALL_TAC
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1456- THEN ASM_REWRITE_TAC[]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:1457: THEN REWRITE_ASM [SYM_th TERM]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1458- THEN IMP_RES_TAC join_elts
##############################################
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1511- lnum_PR_mono_strict
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml:1512: THEN REWRITE_ASM [TERM]
hol88-2.02.19940316/contrib/prog_logic92/exseq.ml-1513- THEN IMP_RES_TAC lnum_plus_inc_strict
##############################################
hol88-2.02.19940316/contrib/prog_logic92/lnum.ml-574- THEN IMP_RES_TAC (REWRITE_RULE[cpo;is_ub;is_lub] lnum_cpo)
hol88-2.02.19940316/contrib/prog_logic92/lnum.ml:575: THEN REWRITE_ASM [lnum_cases4]
hol88-2.02.19940316/contrib/prog_logic92/lnum.ml-576- THEN FIRST_ASSUM (ASSUME_TAC o (SPEC "i:num"))
##############################################
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml-36-
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml:37:let CONV_ASM conv = MAPFILTER_ASSUM (ASSUME_TAC o (CONV_RULE conv));;
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml-38-
##############################################
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml-51-
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml:52:let REWRITE_ASM thl = POP_ASSUM_LIST \asl.REWRITE_ASM_fn (thl) asl;;
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml-53-
##############################################
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml-58-
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml:59:let ONCE_REWRITE_ASM thl = POP_ASSUM_LIST \asl.ONCE_REWRITE_ASM_fn (thl) asl;;
hol88-2.02.19940316/contrib/prog_logic92/mytactics.ml-60-
##############################################
hol88-2.02.19940316/contrib/prog_logic92/wp.ml-276- THEN REPEAT STRIP_TAC
hol88-2.02.19940316/contrib/prog_logic92/wp.ml:277: THEN REWRITE_ASM
hol88-2.02.19940316/contrib/prog_logic92/wp.ml-278- [abort_pair_first
##############################################
hol88-2.02.19940316/contrib/make_use/make_use-1-echo 'loadt`make_use`;; '\
hol88-2.02.19940316/contrib/make_use/make_use:2: 'load_theory`'$1'`;; '\
hol88-2.02.19940316/contrib/make_use/make_use:3: 'make_use`'$1'`;; '\
hol88-2.02.19940316/contrib/make_use/make_use-4- 'quit();;' \
##############################################
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-35- REWRITE_ASM_TAC m n: REWRITE n-th assumption using m-th assumption,
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml:36: then add the result to asm list
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-37-
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml:38: FILTER_REWRITE_ASM A1 A2 As REWRITE_ASMN_TAC but assumptions selected
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-39- are identified by A1 and A2
##############################################
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-109-let FILTER_INFER_ASM_TAC trm inf_rule (asml,g) =
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml:110: let ASM = ASSUME (pick_el trm asml) in
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-111- ASSUME_TAC (inf_rule ASM) (asml,g) ;;
##############################################
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-113-let F_INFER_ASM_TAC trm inf_rule (asml,g) =
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml:114: let ASM = ASSUME (get_match_term trm asml) in
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-115- ASSUME_TAC (inf_rule ASM) (asml,g) ;;
##############################################
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-126-let FILTER_ASM_STRIP_TAC trm (asml,g) =
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml:127: let ASM = SPEC_ALL (ASSUME (pick_el trm asml)) in
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml:128: STRIP_ASSUME_TAC ASM (asml,g) ;;
hol88-2.02.19940316/contrib/WF/MYTACTICS.ml-129-
##############################################
hol88-2.02.19940316/contrib/UNITY/aux_definitions.ml-47- let th_tac = (\(th:thm) (tac:tactic). (UNDISCH_TAC (concl th)) THEN tac) in
hol88-2.02.19940316/contrib/UNITY/aux_definitions.ml:48: let u_asm = (\th:thm. itlist th_tac [th] ALL_TAC)
hol88-2.02.19940316/contrib/UNITY/aux_definitions.ml-49-in
##############################################
hol88-2.02.19940316/contrib/UNITY/examples/mk_example03.ml-444- let th_tac = (\(th:thm) (tac:tactic). (UNDISCH_TAC (concl th)) THEN tac) in
hol88-2.02.19940316/contrib/UNITY/examples/mk_example03.ml:445: let u_asm = (\th:thm. itlist th_tac [th] ALL_TAC)
hol88-2.02.19940316/contrib/UNITY/examples/mk_example03.ml-446-in
##############################################
hol88-2.02.19940316/contrib/Predicate/NOWEB/nountangle.sh-20- -L*) ;; # deliberately ignore requests for #line
hol88-2.02.19940316/contrib/Predicate/NOWEB/nountangle.sh:21: -w[0-9][0-9]*) width=`echo $i | sed 's/^-w//'` ;;
hol88-2.02.19940316/contrib/Predicate/NOWEB/nountangle.sh-22- -) arg="$arg '$i'" ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/predicate.nw-1863- let th1 = SPEC_ALL (RESTRICT_DEF_RULE thm) in
hol88-2.02.19940316/contrib/Predicate/predicate.nw:1864: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/predicate.nw-1865- (GEN_ALL o (DISCH asm) o SPEC_ALL o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/predicate.nw-1877- let th1 = SPEC_ALL thm in
hol88-2.02.19940316/contrib/Predicate/predicate.nw:1878: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/predicate.nw-1879- (GEN_ALL o (DISCH asm) o CONJUNCT1 o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/predicate.nw-1891- let th1 = SPEC_ALL thm in
hol88-2.02.19940316/contrib/Predicate/predicate.nw:1892: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/predicate.nw-1893- (GEN_ALL o (DISCH asm) o CONJUNCT2 o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/predicate.tex-2057- let th1 = SPEC_ALL (RESTRICT_DEF_RULE thm) in
hol88-2.02.19940316/contrib/Predicate/predicate.tex:2058: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/predicate.tex-2059- (GEN_ALL o (DISCH asm) o SPEC_ALL o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/predicate.tex-2075- let th1 = SPEC_ALL thm in
hol88-2.02.19940316/contrib/Predicate/predicate.tex:2076: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/predicate.tex-2077- (GEN_ALL o (DISCH asm) o CONJUNCT1 o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/predicate.tex-2093- let th1 = SPEC_ALL thm in
hol88-2.02.19940316/contrib/Predicate/predicate.tex:2094: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/predicate.tex-2095- (GEN_ALL o (DISCH asm) o CONJUNCT2 o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/my_misc.ml-5- let th1 = SPEC_ALL (RESTRICT_DEF_RULE thm) in
hol88-2.02.19940316/contrib/Predicate/my_misc.ml:6: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/my_misc.ml-7- (GEN_ALL o (DISCH asm) o SPEC_ALL o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/my_misc.ml-9- let th1 = SPEC_ALL thm in
hol88-2.02.19940316/contrib/Predicate/my_misc.ml:10: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/my_misc.ml-11- (GEN_ALL o (DISCH asm) o CONJUNCT1 o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/Predicate/my_misc.ml-13- let th1 = SPEC_ALL thm in
hol88-2.02.19940316/contrib/Predicate/my_misc.ml:14: let asm = fst(dest_imp(concl th1)) in
hol88-2.02.19940316/contrib/Predicate/my_misc.ml-15- (GEN_ALL o (DISCH asm) o CONJUNCT2 o UNDISCH) th1 ;;
##############################################
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-280- let thm2 = GENL ov (DISCH hy thm1) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml:281: let asm = concl thm2 in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-282- let thm3 = SPECL iv (UNDISCH (SPECL ov (ASSUME asm))) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-283- let thm4 = GENL vs (DISCH hy thm3) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml:284: IMP_ANTISYM_RULE (DISCH tm thm2) (DISCH asm thm4);;
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-285-
##############################################
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-608- r2 = REWR_CONV fndef (mk_comb(fn,C')) and
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml:609: asm = AP_TERM fn (ASSUME (mk_eq(C,C'))) and
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-610- v1 = genvar tupty and v2 = genvar tupty in
##############################################
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-691- let rule fn eth th =
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml:692: let asm = (mk_eq o (rand # rand))(dest_eq(fst(dest_imp(concl th)))) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml:693: let imp = (IMP_TRANS (DISCH asm (AP_TERM fn (ASSUME asm))) th) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-694- GEN_ALL (NOT_INTRO(CHOOSE (fn,eth) imp)) in
##############################################
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-714- let rots = mk_rot (map (C SPEC lemma) nums) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml:715: let fn,asm = dest_exists(concl eth) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tyfns.ml-716- let fneqs = map (SYM o SPEC_ALL) (CONJUNCTS (ASSUME asm)) in
##############################################
hol88-2.02.19940316/contrib/rec_tys_listop/Makefile-29- echo 'set_flag(`abort_when_fail`,true);;\
hol88-2.02.19940316/contrib/rec_tys_listop/Makefile:30: compilet `$*`;;\
hol88-2.02.19940316/contrib/rec_tys_listop/Makefile-31- quit();;' | ${Hol}
##############################################
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tydefs.ml-620- let chfn fn v th =
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tydefs.ml:621: let asm = ASSUME (mk_exists(v,find fn (hyp th))) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tydefs.ml-622- CHOOSE (v,asm) th in
##############################################
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tydefs.ml-632- let a1,a2 = CONJ_PAIR(ASSUME ANTE) in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tydefs.ml:633: let asm = MP (SPEC tl (ASSUME res)) a2 in
hol88-2.02.19940316/contrib/rec_tys_listop/rt_lop_tydefs.ml-634- let thm4 = SUBST [SYM (ASSUME def),v] Q (SPECL vs asm) in
##############################################
hol88-2.02.19940316/contrib/AKCL-profiling/profile.lsp-150-(defun prof-offset (addr) (* (/ (float (cadr *current-profile*)) #x10000)
hol88-2.02.19940316/contrib/AKCL-profiling/profile.lsp:151: (- addr (car *current-profile*))))
hol88-2.02.19940316/contrib/AKCL-profiling/profile.lsp-152-
##############################################
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml-180- let imp1 = DISCH tm (SUBST[thm1,v] P thm2) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml:181: let asm = subst[r,l] P in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml:182: let imp2 = DISCH asm (EXISTS (tm,r) (CONJ (REFL r) (ASSUME asm))) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml-183- IMP_ANTISYM_RULE imp1 imp2
##############################################
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml-191- let imp1 = DISCH tm (SUBST[thm2,v] P thm1) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml:192: let asm = subst[r,l] P in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml:193: let imp2 = DISCH asm (EXISTS (tm,r) (CONJ (ASSUME asm) (REFL r))) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml-194- IMP_ANTISYM_RULE imp1 imp2
##############################################
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml-201- let imp1 = DISCH tm (MP (SPEC r (ASSUME tm)) (REFL r)) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml:202: let asm = rand(concl imp1) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml-203- let th1 = SUBST [SYM(ASSUME eq),v] P (ASSUME asm) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml:204: let imp2 = DISCH asm (GEN v (DISCH eq th1)) in
hol88-2.02.19940316/contrib/HOLproof/defs/defs.ml-205- IMP_ANTISYM_RULE imp1 imp2
##############################################
hol88-2.02.19940316/Manual/LaTeX/makeindex.src/troff/makeind-6-out=/dev/null
hol88-2.02.19940316/Manual/LaTeX/makeindex.src/troff/makeind:7:base=`echo $in | sed 's/\(.*\)\..*/\1/'`
hol88-2.02.19940316/Manual/LaTeX/makeindex.src/troff/makeind-8-idx=$base.idx
##############################################
hol88-2.02.19940316/Manual/Tutorial/logic.tex-386-
hol88-2.02.19940316/Manual/Tutorial/logic.tex:387:Executing \ml{new\_theory`$thy$`} creates a new theory called $thy$; it fails
hol88-2.02.19940316/Manual/Tutorial/logic.tex-388-if there already exists a file $thy$\ml{.th} in the current working
##############################################
hol88-2.02.19940316/Manual/Tutorial/parity.tex-555-be selected for rewriting, an \ML\ function {\small\verb%lines%} is defined
hol88-2.02.19940316/Manual/Tutorial/parity.tex:556:such that {\small\verb%lines `%}$l_1\ldots l_n${\small\verb%` %}$t$ is
hol88-2.02.19940316/Manual/Tutorial/parity.tex-557-true whenever $t$ has the
##############################################
hol88-2.02.19940316/Manual/Tutorial/parity.tex-559-for some $l_i$ in the
hol88-2.02.19940316/Manual/Tutorial/parity.tex:560:set specified by the string {\small\verb%`%}$l_1\ldots l_n${\small\verb%`%}.
hol88-2.02.19940316/Manual/Tutorial/parity.tex-561-The functions
##############################################
hol88-2.02.19940316/Manual/Tutorial/tool.tex-751-function composition operator \ml{o}
hol88-2.02.19940316/Manual/Tutorial/tool.tex:752:(where \ml{(}$f$~\ml{o}~$g$\ml{)}$x$~\ml{=}~$g$\ml{(}$f$\ml{(}$x$\ml{))}).
hol88-2.02.19940316/Manual/Tutorial/tool.tex-753-
##############################################
hol88-2.02.19940316/Manual/Tutorial/tool.tex-1012-normalizing all subterms that are conjunctions. However the functions
hol88-2.02.19940316/Manual/Tutorial/tool.tex:1013:\ml{CONJ\_NORM\_CONV}{\small $n$} (where {\small $n = 2,3,4$}) all
hol88-2.02.19940316/Manual/Tutorial/tool.tex-1014-fail on non-conjunctions.
##############################################
hol88-2.02.19940316/Manual/Tutorial/intro.tex-237-by always setting {\small\verb%HOLPATH%} or by typing:
hol88-2.02.19940316/Manual/Tutorial/intro.tex:238:{\small\verb%install `%}{\small$path$}{\small\verb%/hol`;;%}
hol88-2.02.19940316/Manual/Tutorial/intro.tex-239-whenever you start (for a suitable string {\small $path$}), \eg\
##############################################
hol88-2.02.19940316/Manual/Reference/bin/doc-to-tex-14-#
hol88-2.02.19940316/Manual/Reference/bin/doc-to-tex:15:# for file in `cd $1; ls -1 *.doc | sed 's/.doc$//g' | sort -f`
hol88-2.02.19940316/Manual/Reference/bin/doc-to-tex-16-# do
##############################################
hol88-2.02.19940316/Manual/Reference/bin/jac-to-tex-12-
hol88-2.02.19940316/Manual/Reference/bin/jac-to-tex:13:for file in `cd $1; ls -1 *.jac | sed -e 's/.jac$//g' | sort -f`
hol88-2.02.19940316/Manual/Reference/bin/jac-to-tex-14- do
##############################################
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2~-23- do map create_doc_file (thl@axl@del) in
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2~:24: let ok = (new_theory \`dummy$$\`; new_parent \`$1\`; true) ? false in
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2~-25- print_string \`!!\`; print_newline();
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2~:26: ok => create_doc_files \`$1\` | print_string \`echo Failed\`;
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2~-27- print_newline(); print_string \`??\`; print_newline();
##############################################
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2-26- do map create_doc_file (thl@axl@del) in
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2:27: let ok = (new_theory \`dummy$$\`; new_parent \`$1\`; true) ? false in
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2-28- print_string \`!!\`; print_newline();
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2:29: ok => create_doc_files \`$1\` | print_string \`echo Failed\`;
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2-30- print_newline(); print_string \`??\`; print_newline();
##############################################
hol88-2.02.19940316/Manual/Reference/bin/libfield-7-
hol88-2.02.19940316/Manual/Reference/bin/libfield:8:for i in `shift; echo $*`; do
hol88-2.02.19940316/Manual/Reference/bin/libfield-9-(cat | ed - $i) <<+
##############################################
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2.old-23- do map create_doc_file (thl@axl@del) in
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2.old:24: let ok = (new_theory \`dummy$$\`; new_parent \`$1\`; true) ? false in
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2.old-25- print_string \`!!\`; print_newline();
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2.old:26: ok => create_doc_files \`$1\` | print_string \`echo Failed\`;
hol88-2.02.19940316/Manual/Reference/bin/create-doc-files2.old-27- print_newline(); print_string \`??\`; print_newline();
##############################################
hol88-2.02.19940316/Manual/Reference/.save/doc-to-tex-13-#
hol88-2.02.19940316/Manual/Reference/.save/doc-to-tex:14:# for file in `cd $1; ls -1 *.doc | sed 's/.doc$//g' | sort -f`
hol88-2.02.19940316/Manual/Reference/.save/doc-to-tex-15-# do
##############################################
hol88-2.02.19940316/Manual/Reference/.save/jac-to-tex-12-
hol88-2.02.19940316/Manual/Reference/.save/jac-to-tex:13:for file in `cd $1; ls -1 *.jac | sed -e 's/.jac$//g' | sort -f`
hol88-2.02.19940316/Manual/Reference/.save/jac-to-tex-14- do
##############################################
hol88-2.02.19940316/Manual/Reference/tactics.tex-1832-{\par\samepage\setseps\small\begin{verbatim}
hol88-2.02.19940316/Manual/Reference/tactics.tex:1833: FIRST_ASSUM (\asm. CONTR_TAC asm ORELSE ACCEPT_TAC asm)
hol88-2.02.19940316/Manual/Reference/tactics.tex-1834-\end{verbatim}}
##############################################
hol88-2.02.19940316/Manual/Reference/entries.tex-8585-\begin{verbatim}
hol88-2.02.19940316/Manual/Reference/entries.tex:8586: FIRST_ASSUM (\asm. CONTR_TAC asm ORELSE ACCEPT_TAC asm)
hol88-2.02.19940316/Manual/Reference/entries.tex-8587-\end{verbatim}
##############################################
hol88-2.02.19940316/Manual/Reference/entries.tex-11693-
hol88-2.02.19940316/Manual/Reference/entries.tex:11694:#is_binder `$?!`;;
hol88-2.02.19940316/Manual/Reference/entries.tex-11695-false : bool
##############################################
hol88-2.02.19940316/Manual/Reference/entries.tex-11837-
hol88-2.02.19940316/Manual/Reference/entries.tex:11838:#is_constant `$!`;;
hol88-2.02.19940316/Manual/Reference/entries.tex-11839-false : bool
##############################################
hol88-2.02.19940316/Manual/Reference/entries.tex-12076-\begin{verbatim}
hol88-2.02.19940316/Manual/Reference/entries.tex:12077:#is_infix `$+`;;
hol88-2.02.19940316/Manual/Reference/entries.tex-12078-false : bool
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-26-
hol88-2.02.19940316/Manual/Description/ml7.tex:27:\noindent Executing \ml{openi\ `$file$`} returns a string that can be used by
hol88-2.02.19940316/Manual/Description/ml7.tex-28-the function \ml{read} (see below) to read characters from the file $file$; and
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-36-
hol88-2.02.19940316/Manual/Description/ml7.tex:37:\noindent Executing \ml{read\ `$port$`} reads a character from a port $port$
hol88-2.02.19940316/Manual/Description/ml7.tex-38-which has been produced with \ml{openi}.
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-50-
hol88-2.02.19940316/Manual/Description/ml7.tex:51:\noindent Executing \ml{openw\ `$file$`} creates a new file named $file$ for
hol88-2.02.19940316/Manual/Description/ml7.tex-52-output (overwriting an existing file with the same name) and returns a string
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-54-
hol88-2.02.19940316/Manual/Description/ml7.tex:55:To evaluate \ml{append\_openw `$file$`}: if no file named $file$ exists, a new
hol88-2.02.19940316/Manual/Description/ml7.tex-56-one is created and a port for writing to it opened. If a file named $file$
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-66-
hol88-2.02.19940316/Manual/Description/ml7.tex:67:\noindent Executing \ml{write(`$port$`,`$chars$`)} writes $chars$ to port
hol88-2.02.19940316/Manual/Description/ml7.tex-68-$port$ (which must have been produced by \ml{openw} or \ml{append\_openw}).
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-182-
hol88-2.02.19940316/Manual/Description/ml7.tex:183:Evaluating \ml{load(`$filename$`,$prflag$)} reads phrases from the first file
hol88-2.02.19940316/Manual/Description/ml7.tex-184-named $filename$ on the current search path and evaluates them exactly as if
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-561-{\small
hol88-2.02.19940316/Manual/Description/ml7.tex:562:\noindent\ml{\ \ \ autoload(`$x$`,\ `$fun$`,\ [`$s_1$`;$\ \ldots\ $;`$s_n$`])}
hol88-2.02.19940316/Manual/Description/ml7.tex-563-}
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-568-declaration or expression $E$, the \ML\ application
hol88-2.02.19940316/Manual/Description/ml7.tex:569:\ml{$fun$[`$s_1$`;$\ \ldots\ $;`$s_n$`]} is evaluated before $E$ is evaluated.
hol88-2.02.19940316/Manual/Description/ml7.tex-570-In the session below, the various
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-656-{\small
hol88-2.02.19940316/Manual/Description/ml7.tex:657:\noindent\ \ \ \ml{let\_before(`$MLname$`, `$MLfn$`,[`$s_1$`;$\ldots$;`$s_n$`])}
hol88-2.02.19940316/Manual/Description/ml7.tex-658-}
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-667-
hol88-2.02.19940316/Manual/Description/ml7.tex:668:\noindent\ \ \ \ml{let $MLname$ = $MLfn$[`$s_1$`;$\ \ldots\ $;`$s_n$`]}
hol88-2.02.19940316/Manual/Description/ml7.tex-669-}
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-878-
hol88-2.02.19940316/Manual/Description/ml7.tex:879:\ml{link(`$old$`,`$new$`)} links the file $old$ to $new$; and fails
hol88-2.02.19940316/Manual/Description/ml7.tex-880-if $old$ does not exist.
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-1205-
hol88-2.02.19940316/Manual/Description/ml7.tex:1206:\noindent This function takes a pair \ml{(`$flag$`,$b$)},
hol88-2.02.19940316/Manual/Description/ml7.tex-1207- where $b$ is \ml{true} or \ml{false}, and
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-1254-
hol88-2.02.19940316/Manual/Description/ml7.tex:1255:\noindent Executing \ml{set\_prompt `}$string$\ml{`}
hol88-2.02.19940316/Manual/Description/ml7.tex-1256-changes the ML prompt to $string$;
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-1376-\end{verbatim}\end{boxed}
hol88-2.02.19940316/Manual/Description/ml7.tex:1377:Evaluating \ml{help `$foo$`} concatenates the
hol88-2.02.19940316/Manual/Description/ml7.tex-1378-contents of the help file associated with \ml{$foo$} into the
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-1406-\noindent This installs a new user-supplied help function, and returns the
hol88-2.02.19940316/Manual/Description/ml7.tex:1407:previous one as result. The effect of \ml{help `$file$`} is to pipe the
hol88-2.02.19940316/Manual/Description/ml7.tex-1408-appropriate help file derived from $file${\small\verb%.doc%} into the current
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-1467-\begin{hol}
hol88-2.02.19940316/Manual/Description/ml7.tex:1468:{\small\verb% new_syntax_block(`XXX`, `YYY`, `%}$f${\small\verb%`);;%}
hol88-2.02.19940316/Manual/Description/ml7.tex-1469-\end{hol}
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-1522-
hol88-2.02.19940316/Manual/Description/ml7.tex:1523:Executing \ml{install `$directory$`} does the following:
hol88-2.02.19940316/Manual/Description/ml7.tex-1524-
##############################################
hol88-2.02.19940316/Manual/Description/ml7.tex-1527-\item Sets the search path to:
hol88-2.02.19940316/Manual/Description/ml7.tex:1528:{\small\verb%[``; `~/`; `%}\ml{$directory$}{\small\verb%/theories/`]%}%
hol88-2.02.19940316/Manual/Description/ml7.tex-1529-\index{search path!for \HOL\ system}%
##############################################
hol88-2.02.19940316/Manual/Description/description.idx-83-\indexentry{list concatenation, in ML@list concatenation, in \ML}{12}
hol88-2.02.19940316/Manual/Description/description.idx:84:\indexentry{ string markers@{\small\verb+`+ $\cdots$ \verb+`+} (string markers, in \ML)}{13}
hol88-2.02.19940316/Manual/Description/description.idx-85-\indexentry{polymorphism, in ML@polymorphism, in \ML|(}{13}
##############################################
hol88-2.02.19940316/Manual/Description/description.idx-301-\indexentry{strings, in ML@strings, in \ML}{29}
hol88-2.02.19940316/Manual/Description/description.idx:302:\indexentry{ string markers@{\small\verb+`+ $\cdots$ \verb+`+} (string markers, in \ML)}{29}
hol88-2.02.19940316/Manual/Description/description.idx-303-\indexentry{ escape, in ML strings@{\small\verb+\+} (escape, in \ML\ strings)}{29}
##############################################
hol88-2.02.19940316/Manual/Description/logic.tex-797-Suppose $t$ is a term, with canonical context $\alpha\!s,\!x\!s$ say,
hol88-2.02.19940316/Manual/Description/logic.tex:798:where $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$
hol88-2.02.19940316/Manual/Description/logic.tex:799:and where for $j=1,\ldots,m$ the type of the variable $x_j$ is
hol88-2.02.19940316/Manual/Description/logic.tex-800-$\sigma_j$. If $\alpha\!s'.\tau_{i}$ ($i=1,\ldots,n$) are
##############################################
hol88-2.02.19940316/Manual/Description/logic.tex-846-Suppose $t$ is a term, with canonical context $\alpha\!s,\!x\!s$ say,
hol88-2.02.19940316/Manual/Description/logic.tex:847:where $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$
hol88-2.02.19940316/Manual/Description/logic.tex:848:and where for $j=1,\ldots,m$ the type of the variable $x_j$ is
hol88-2.02.19940316/Manual/Description/logic.tex-849-$\sigma_j$. If one has terms-in-context $\alpha\!s,\!x\!s'.t_{j}$ for
##############################################
hol88-2.02.19940316/Manual/Description/logic.tex-967-\]
hol88-2.02.19940316/Manual/Description/logic.tex:968:where $f^{-1}\{1\}=\{x\in X : f(x)=1\}$. (Note that $f^{-1}\{1\}$ is in
hol88-2.02.19940316/Manual/Description/logic.tex-969-$\cal U$ when it is non-empty, by the property {\bf Sub} of the
##############################################
hol88-2.02.19940316/Manual/Description/logic.tex-982-standard collection of logical constants includes $\T$ (`true'), $\F$
hol88-2.02.19940316/Manual/Description/logic.tex:983:(`false')\index{truth values, in HOL logic@truth values, in \HOL\ logic!abstract form of}, $\imp$ (`implies'), $\wedge$ (`and'), $\vee$
hol88-2.02.19940316/Manual/Description/logic.tex:984:(`or'), $\neg$ (`not'), $\forall$ (`for all'), $\exists$ (`there
hol88-2.02.19940316/Manual/Description/logic.tex:985:exists'), $=$ (`equals'), $\iota$ (`the'), and $\hilbert$ (`a'). This
hol88-2.02.19940316/Manual/Description/logic.tex-986-set is redundant, since it can be defined (in a sense explained in
##############################################
hol88-2.02.19940316/Manual/Description/ml1.tex-425-A sequence of characters enclosed between string quotes
hol88-2.02.19940316/Manual/Description/ml1.tex:426:({\small\verb%`%} -- i.e. ascii 96)\index{ string markers@{\small\verb+`+ $\cdots$ \verb+`+} (string markers, in \ML)} is a string.
hol88-2.02.19940316/Manual/Description/ml1.tex-427-
##############################################
hol88-2.02.19940316/Manual/Description/ml1.tex-552-yielding a string\index{strings, in ML@strings, in \ML!to identify failures}\index{failure strings, in ML@failure strings, in \ML|(} (which is usually the function name) to identify the sort
hol88-2.02.19940316/Manual/Description/ml1.tex:553:of failure. A failure with string {\small\verb%`%}$t${\small\verb%`%}
hol88-2.02.19940316/Manual/Description/ml1.tex-554-may also be generated explicitly by evaluating the expression
hol88-2.02.19940316/Manual/Description/ml1.tex:555:{\small\verb%failwith `%}$t${\small\verb%`%}
hol88-2.02.19940316/Manual/Description/ml1.tex-556-\index{failwith@\ml{failwith}} (or more
##############################################
hol88-2.02.19940316/Manual/Description/ml2.tex-426-string quotes ({\small\verb%`%}), \eg\\
hol88-2.02.19940316/Manual/Description/ml2.tex:427:{\small\verb%`This is a single string`%}.\index{ string markers@{\small\verb+`+ $\cdots$ \verb+`+} (string markers, in \ML)}
hol88-2.02.19940316/Manual/Description/ml2.tex-428-In any string the occurrence of {\small\verb%\%}$x$\index{ escape, in ML strings@{\small\verb+\+} (escape, in \ML\ strings)} has the following meanings for
##############################################
hol88-2.02.19940316/Manual/Description/ml3.tex-48-fails implicitly with failure string {\small\verb%`div`%}, whilst that of
hol88-2.02.19940316/Manual/Description/ml3.tex:49:{\small\verb%failwith `%}$str${\small\verb%`%} fails explicitly with
hol88-2.02.19940316/Manual/Description/ml3.tex-50-failure string
hol88-2.02.19940316/Manual/Description/ml3.tex:51:{\small\verb%`%}$str${\small\verb%`%}. We shall say two evaluations fail
hol88-2.02.19940316/Manual/Description/ml3.tex-52- {\it similarly\/}\index{failure, in ML@failure, in \ML!similar} if
##############################################
hol88-2.02.19940316/Manual/Description/ml3.tex-234-evaluation of $p${\small\verb%=%}$e$ fails with failure string
hol88-2.02.19940316/Manual/Description/ml3.tex:235:{\small\verb%`%}$pattern${\small\verb%`%}.\index{bindings, in ML@bindings, in \ML!in function definitions|)}\index{bindings, in ML@bindings, in \ML!evaluation of|)}
hol88-2.02.19940316/Manual/Description/ml3.tex-236-
##############################################
hol88-2.02.19940316/Manual/Description/ml3.tex-409-the assignment fails similarly. If the matching to $p$ fails, then
hol88-2.02.19940316/Manual/Description/ml3.tex:410:the assignment fails with {\small\verb%`%}$pattern${\small\verb%`%}. The
hol88-2.02.19940316/Manual/Description/ml3.tex-411-value of $p${\small\verb%:=%}$e$ is the value of $e$.
##############################################
hol88-2.02.19940316/Manual/Description/ml3.tex-568-variable in $p_i$ to the corresponding components of $E$. If no
hol88-2.02.19940316/Manual/Description/ml3.tex:569:match succeeds, the evaluation fails with {\small\verb%`%}$pattern${\small\verb%`%}.
hol88-2.02.19940316/Manual/Description/ml3.tex-570-
##############################################
hol88-2.02.19940316/Manual/Description/semantics.tex-965-variables occurring in the formula $t$. Then $\alpha\!s,\!x\!s.t$ is a
hol88-2.02.19940316/Manual/Description/semantics.tex:966:term-in-context, where $x\!s=x_{1},\ldots,x_{n}$. (Change any bound
hol88-2.02.19940316/Manual/Description/semantics.tex-967-variables in $t$ to make them distinct from $x\!s$ if necessary.)
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-246-The evaluation of
hol88-2.02.19940316/Manual/Description/system.tex:247:\ml{mk\_type(`}$name$\ml{`,\ [}$\sigma_1$\ml{;}$\cdots$\ml{;}$\sigma_n$\ml{])}
hol88-2.02.19940316/Manual/Description/system.tex-248-fails if
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-566-Type variable &
hol88-2.02.19940316/Manual/Description/system.tex:567:{\small\verb%":*%}$\cdots${\small\verb%"%} & {\small\verb%mk_vartype(`*%}$\cdots${\small\verb%`)%} \\ \hline
hol88-2.02.19940316/Manual/Description/system.tex-568-Type constant &
hol88-2.02.19940316/Manual/Description/system.tex:569:{\small\verb%":%}$op${\small\verb%"%} & {\small\verb%mk_type(`%}$op${\small\verb%`,[])%} \\ \hline
hol88-2.02.19940316/Manual/Description/system.tex-570-Function type &
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-574-{\small\verb%":(%}$\sigma_1${\small\verb%,%} $\ldots$ {\small\verb%,%} $\sigma_n${\small\verb%)%}$op${\small\verb%"%} &
hol88-2.02.19940316/Manual/Description/system.tex:575:{\small\verb%mk_type(`%}$op${\small\verb%`, [":%}$\sigma_1${\small\verb%";%} $\ldots$ {\small\verb%;":%}$\sigma_n${\small\verb%"])%}
hol88-2.02.19940316/Manual/Description/system.tex-576-\\ \hline
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-611-Variable & {\small\verb%"%}$var${\small\verb%:%}$\sigma${\small\verb%"%} &
hol88-2.02.19940316/Manual/Description/system.tex:612:{\small\verb%mk_var(`%}$var${\small\verb%`,":%}$\sigma${\small\verb%")%} \\ \hline
hol88-2.02.19940316/Manual/Description/system.tex-613-Constant & {\small\verb%"%}$const${\small\verb%:%}$\sigma${\small\verb%"%} &
hol88-2.02.19940316/Manual/Description/system.tex:614:{\small\verb%mk_const(`%}$const${\small\verb%`,":%}$\sigma${\small\verb%")%} \\ \hline
hol88-2.02.19940316/Manual/Description/system.tex-615-Combination & {\small\verb%"%}$t_1\ t_2${\small\verb%"%} &
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-862-\begin{hol}
hol88-2.02.19940316/Manual/Description/system.tex:863:{\small\verb% associate_restriction(`%}$c${\small\verb%`, `RES_%}$c${\small\verb%`)%}
hol88-2.02.19940316/Manual/Description/system.tex-864-\end{hol}
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1740-
hol88-2.02.19940316/Manual/Description/system.tex:1741:\noindent \ml{new\_theory `$thy$`} can be done in both
hol88-2.02.19940316/Manual/Description/system.tex-1742-proof\index{proof mode, in HOL system@proof mode, in \HOL\ system} and
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1791-
hol88-2.02.19940316/Manual/Description/system.tex:1792:\noindent Executing {\small\verb%new_constant(`%}$c${\small\verb%`,%}$\sigma${\small\verb%)%} makes
hol88-2.02.19940316/Manual/Description/system.tex-1793-$c_{\sigma'}$ a new constant\index{constants, in HOL logic@constants, in \HOL\ logic!declaration of} of the current theory,
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1809-
hol88-2.02.19940316/Manual/Description/system.tex:1810:\noindent Executing \ml{new\_infix(`}$ix$\ml{`,}$\sigma$\ml{)}
hol88-2.02.19940316/Manual/Description/system.tex-1811-declares $ix$ to be a new constant with generic type $\sigma$ and
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1827-
hol88-2.02.19940316/Manual/Description/system.tex:1828:\noindent Executing \ml{new\_binder(`}$b$\ml{`,}$\sigma$\ml{)}\index{binders, in HOL logic@binders, in \HOL\ logic!declaration of}
hol88-2.02.19940316/Manual/Description/system.tex-1829-declares $b$ to be a new constant with generic type $\sigma$ and
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1844-
hol88-2.02.19940316/Manual/Description/system.tex:1845:\noindent Executing \ml{new\_axiom(`}$name$\ml{`,}$t$\ml{)} declares the
hol88-2.02.19940316/Manual/Description/system.tex-1846-sequent
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1864-\noindent
hol88-2.02.19940316/Manual/Description/system.tex:1865:Evaluating \ml{save\_thm(`}$name$\ml{`,}$th$\ml{)} will save the theorem\index{theorems, in HOL logic@theorems, in \HOL\ logic!saving of}\index{saving theorems}
hol88-2.02.19940316/Manual/Description/system.tex-1866-$th$ with name $name$ in the current theory segment.
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1923-\noindent Evaluating
hol88-2.02.19940316/Manual/Description/system.tex:1924: \ml{new\_definition(`}$name$\ml{`,\ "}$c\ v_1\ \cdots\ v_n\ =\ t$\ml{")},
hol88-2.02.19940316/Manual/Description/system.tex-1925-where $c$ is not already a constant, declares the sequent
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1963-\begin{hol}
hol88-2.02.19940316/Manual/Description/system.tex:1964:{\small\verb% new_infix_definition(`%}$ix${\small\verb%_DEF`, "%}$m$ $ix$ $n${\small\verb% = ... ")%}
hol88-2.02.19940316/Manual/Description/system.tex-1965-\end{hol}
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1971-\begin{hol}
hol88-2.02.19940316/Manual/Description/system.tex:1972:{\small\verb% new_infix_definition(`%}$ix${\small\verb%_DEF`, "%}$ix$ $m$ $n${\small\verb% = ... ")%}
hol88-2.02.19940316/Manual/Description/system.tex-1973-\end{hol}
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-1982-\begin{hol}
hol88-2.02.19940316/Manual/Description/system.tex:1983:{\small\verb% new_infix_definition(`%}$ix${\small\verb%_DEF`, "$%}$ix$ $m$ $n${\small\verb% = ... ")%}
hol88-2.02.19940316/Manual/Description/system.tex-1984-\end{hol}
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-2031- \ml{new\_specification}\\
hol88-2.02.19940316/Manual/Description/system.tex:2032:\ \ml{`}$name$\ml{`}\\
hol88-2.02.19940316/Manual/Description/system.tex:2033:\ \ml{[`}$flag_1$\ml{`,`}$c_1$\ml{`;\ }$\ldots$\ml{\ ;\ `}$flag_n$\ml{`,`}$c_n$\ml{`]}\\
hol88-2.02.19940316/Manual/Description/system.tex-2034-\ \ml{|-\ ?}$x_1\ \cdots\ x_n$\ml{.}\ $t$\ml{[}$x_1$\ml{,}$\ \ldots\
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-2047-
hol88-2.02.19940316/Manual/Description/system.tex:2048:\noindent If \ml{`}$flag_i$\ml{`} is \ml{`constant`}
hol88-2.02.19940316/Manual/Description/system.tex-2049-then $c_i$ is declared an ordinary constant, if it is
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-2986-
hol88-2.02.19940316/Manual/Description/system.tex:2987:\noindent Evaluating \ml{new\_type\_abbrev(`}$name$\ml{`,":}$\sigma$\ml{")}
hol88-2.02.19940316/Manual/Description/system.tex-2988-enables $name$ to be used in quotations instead of $\sigma$. The evaluation
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-5378-parser) to $c_i$, which must be an existing constant (`$a$' is for
hol88-2.02.19940316/Manual/Description/system.tex:5379:`abbreviation' and `$c$' for `constant').
hol88-2.02.19940316/Manual/Description/system.tex-5380-
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-5725-
hol88-2.02.19940316/Manual/Description/system.tex:5726:\noindent Evaluating \ml{hide\_constant\ `}$x$\ml{`}
hol88-2.02.19940316/Manual/Description/system.tex-5727-makes the quotation parser treat $x$ as a variable (lexical
##############################################
hol88-2.02.19940316/Manual/Description/system.tex-5781-\noindent Evaluating
hol88-2.02.19940316/Manual/Description/system.tex:5782:\ml{autoload\_theory(`}$kind$\ml{`,`}$thy$\ml{`,`}$name$\ml{`)}, where $kind$
hol88-2.02.19940316/Manual/Description/system.tex-5783-is \ml{axiom}, \ml{definition} or \ml{theorem}, has the side effect of setting
##############################################
hol88-2.02.19940316/Manual/Description/tactics.tex-1543-
hol88-2.02.19940316/Manual/Description/tactics.tex:1544:Suppose \ml{$T_1\ g$ = ($gl$,$p$)} where \ml{$gl$=[$g_1$;$\ldots$;$g_n$]}.
hol88-2.02.19940316/Manual/Description/tactics.tex-1545-Suppose also that
##############################################
hol88-2.02.19940316/Manual/Description/version2.tex-730-\begin{hol}
hol88-2.02.19940316/Manual/Description/version2.tex:731:\ml{ new\_syntax\_block(`XXX`, `YYY`, `}$f$\ml{`);;}
hol88-2.02.19940316/Manual/Description/version2.tex-732-\end{hol}
##############################################
hol88-2.02.19940316/Manual/Description/version2.tex-1539- DEPTH_FORALL_CONV OR_IMP mk_injs
hol88-2.02.19940316/Manual/Description/version2.tex:1540: DO_ASM PROJ mk_new_vars
hol88-2.02.19940316/Manual/Description/version2.tex-1541- ELIM_ANTE_EQNS_CONV RM_LEN_CONV mk_subset_pred
##############################################
hol88-2.02.19940316/Manual/Description/index.tex-70- \item {\small\verb+^+} (string concatenation, in \ML), \pin{66}
hol88-2.02.19940316/Manual/Description/index.tex:71: \item {\small\verb+`+ $\cdots$ \verb+`+} (string markers, in \ML), 13,
hol88-2.02.19940316/Manual/Description/index.tex-72- 29
##############################################
hol88-2.02.19940316/Manual/Guide/guide.tex-776-example, the \meta{name} field for the tactical {\small\verb!THEN!} should be
hol88-2.02.19940316/Manual/Guide/guide.tex:777:`{\small\verb!$THEN!}', not `{\small\verb!THEN!}'. The {\small\verb!\TYPE!}
hol88-2.02.19940316/Manual/Guide/guide.tex-778-line is a required field in every \doc\ file. There must be exactly one
##############################################
hol88-2.02.19940316/Manual/Guide/oldguide.tex-723-example, the \meta{name} field for the tactical {\small\verb!THEN!} should be
hol88-2.02.19940316/Manual/Guide/oldguide.tex:724:`{\small\verb!$THEN!}', not `{\small\verb!THEN!}'. The {\small\verb!\TYPE!}
hol88-2.02.19940316/Manual/Guide/oldguide.tex-725-line is a required field in every \doc\ file. There must be exactly one
##############################################
hol88-2.02.19940316/Training/course/logicA.tex-576-\bpindent\LARGE{\bf
hol88-2.02.19940316/Training/course/logicA.tex:577:and so `$I \; 7$' and `$I \; T$' are both well-typed.}
hol88-2.02.19940316/Training/course/logicA.tex-578-\epindent
##############################################
hol88-2.02.19940316/Training/exercises/exercises/rules.ml-23- let x,tm = dest_exists (dest_neg (concl th)) in
hol88-2.02.19940316/Training/exercises/exercises/rules.ml:24: let asm = EXISTS (rand (concl th), x) (ASSUME tm) in
hol88-2.02.19940316/Training/exercises/exercises/rules.ml-25- GEN x (NOT_INTRO (DISCH tm (MP th asm)));;
##############################################
hol88-2.02.19940316/Training/exercises/exercises/rules.ml-41-% --------------------------------------------------------------------- %
hol88-2.02.19940316/Training/exercises/exercises/rules.ml:42:let asm = EXISTS (rand (concl th), x) (ASSUME tm);;
hol88-2.02.19940316/Training/exercises/exercises/rules.ml-43-
##############################################
hol88-2.02.19940316/Training/exercises/exercises/rules.ml-49-% --------------------------------------------------------------------- %
hol88-2.02.19940316/Training/exercises/exercises/rules.ml:50:% Now, asm and th form a contradiction. Modus ponens works on negations %
hol88-2.02.19940316/Training/exercises/exercises/rules.ml-51-% so we can just do the following to derive falsity: %
##############################################
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-24- let x,tm = dest_exists (dest_neg (concl th)) in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml:25: let asm = EXISTS (rand (concl th), x) (ASSUME tm) in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-26- GEN x (NOT_INTRO (DISCH tm (MP th asm)));;
##############################################
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-42-% --------------------------------------------------------------------- %
hol88-2.02.19940316/Training/exercises/solutions/rules.ml:43:let asm = EXISTS (rand (concl th), x) (ASSUME tm);;
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-44-
##############################################
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-50-% --------------------------------------------------------------------- %
hol88-2.02.19940316/Training/exercises/solutions/rules.ml:51:% Now, asm and th form a contradiction. Modus ponens works on negations %
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-52-% so we can just do the following to derive falsity: %
##############################################
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-79- let x,tm = (I # dest_neg) (dest_forall (concl th)) in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml:80: let asm = ASSUME (mk_exists (x,tm)) in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml:81: let sthm = SELECT_RULE asm in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-82- let fthm = MP (SPEC (rand (concl sthm)) th) sthm in
##############################################
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-89- let x,tm = (I # dest_neg) (dest_forall (concl th)) in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml:90: let asm = MP (SPEC x th) (ASSUME tm) in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml:91: let cth = CHOOSE (x,ASSUME (mk_exists(x,tm))) asm in
hol88-2.02.19940316/Training/exercises/solutions/rules.ml-92- NOT_INTRO (DISCH (mk_exists(x,tm)) cth);;
##############################################
hol88-2.02.19940316/Training/exercises/solutions/forward.ml-316-let th5 =
hol88-2.02.19940316/Training/exercises/solutions/forward.ml:317: let asm = ASSUME "!y x. P(x:*,y:**)" in
hol88-2.02.19940316/Training/exercises/solutions/forward.ml-318- let thm = GENL ["x:*";"y:**"] (SPECL ["y:**";"x:*"] asm) in
##############################################
hol88-2.02.19940316/Training/exercises/solutions/conv.ml-39- let imp1 = DISCH tm (GEN x (AP_THM (ASSUME tm) x)) in
hol88-2.02.19940316/Training/exercises/solutions/conv.ml:40: let asm = ASSUME (concl (GEN x (AP_THM (ASSUME tm) x))) in
hol88-2.02.19940316/Training/exercises/solutions/conv.ml-41- IMP_ANTISYM_RULE imp1 (DISCH_ALL (EXT asm))
##############################################
hol88-2.02.19940316/Training/studies/int_mod/doing_alg_paper/ApA.tex-82-\end{center}
hol88-2.02.19940316/Training/studies/int_mod/doing_alg_paper/ApA.tex:83:where ${\cal T}_i$ is the theorem {\tt $A_i$ |- $t_i$ = $u_i$} and where the
hol88-2.02.19940316/Training/studies/int_mod/doing_alg_paper/ApA.tex-84-term $t[x_1,\ldots,x_n]$ serves as a template for the substitution. The
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-11-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:12:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:13: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-14- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-34-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:35:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:36: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-37- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-56-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:57:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:58: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-59- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-79-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:80:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:81: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-82- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-105-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:106:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:107: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-108- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-126-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:127:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:128: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-129- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-148-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:149:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:150: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-151- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-171-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:172:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:173: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-174- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-196-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:197:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:198: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-199- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-218-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:219:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:220: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-221- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-241-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:242:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:243: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-244- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-261-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:262:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:263: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-264- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-282-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:283:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:284: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-285- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-302-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:303:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:304: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-305- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-327-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:328:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:329: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-330- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-351-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:352:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex:353: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/apx.tex-354- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-423-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:424:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:425: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-426- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-492-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:493:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:494: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-495- AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-521-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:522:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:523: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-524- AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-566-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:567:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:568: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-569- AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-617-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:618:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex:619: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/asyn.tex-620- AsynSystem rep (idreq,mpc,mar,pc,acc,ir,rtn,arg,buf,idack,dack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/plan.tex-52-|- \(\forall\)datain pwr dataout wmem dreq addr.
hol88-2.02.19940316/Training/studies/microprocessor/plan.tex:53: Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/plan.tex:54: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/plan.tex-55- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-118-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:119:|- Val3_CASES_ASM REP16
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-120-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:121:|- Val4Word4_ASM REP16
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-122-\endtt
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-195-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:196:let INC_ASM = new_definition (
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-197- `INC_ASM`,
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:198: "INC_ASM n (rep:^rep_ty) =
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-199- \(\forall\)w. ((valn rep) ((inc rep) w)) = ((((valn rep) w) + 1) MOD (2 EXP n))");;
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-237-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:238:let ISZERO_ASM = new_definition (
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-239-`ISZERO_ASM`,
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:240: "ISZERO_ASM (rep:^rep_ty) =
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-241- \(\forall\)w. ((iszero rep) w) = (((valn rep) w) = 0)");;
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-242-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:243:let ADD_ASM = new_definition (
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-244- `ADD_ASM`,
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:245: "ADD_ASM n (rep:^rep_ty) =
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-246- \(\forall\)w1 w2.
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-249-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:250:let SUB_ASM = new_definition (
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-251- `SUB_ASM`,
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:252: "SUB_ASM n (rep:^rep_ty) =
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-253- \(\forall\)w1 w2.
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-256-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:257:let FETCH_STORE_ASM = new_definition (
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-258- `FETCH_STORE_ASM`,
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:259: "FETCH_STORE_ASM (rep:^rep_ty) =
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-260- \(\forall\)m a1 a2 w.
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-274-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:275:|- INC_ASM 16 REP16
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-276-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:277:|- ISZERO_ASM REP16
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-278-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:279:|- ADD_ASM 16 REP16
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-280-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:281:|- SUB_ASM 16 REP16
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-282-
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex:283:|- FETCH_STORE_ASM REP16
hol88-2.02.19940316/Training/studies/microprocessor/relate.tex-284-\endtt
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-137- \(\forall\)ireq mpc mar pc acc ir rtn arg buf iack mem.
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:138: Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:139: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-140- SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-168-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:169:|- Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:170: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-171- SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-314- [ "((val4 rep) o mpc) Eq 0 = g" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:315: [ "Val3_CASES_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:316: [ "Val4Word4_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-317- [ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-332- [ "((val4 rep) o mpc) Eq 0 = g" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:333: [ "Val3_CASES_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:334: [ "Val4Word4_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-335- [ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-348- [ "((val4 rep) o mpc) Eq 0 = g" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:349: [ "Val3_CASES_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:350: [ "Val4Word4_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-351- [ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-365-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:366:|- Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex:367: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/temp.tex-368- SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-87- [],
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:88: "Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:89: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-90- TamarackImp rep (
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-152- (dreq t = F)"
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:153: [ "Val3_CASES_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:154: [ "Val4Word4_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-155- [ "NextMPC
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-445-
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:446:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:447: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-448- TamarackImp
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-619- \(\forall\)ireq mpc mar pc acc ir rtn arg buf iack mem.
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:620: Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:621: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-622- SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-685- ADD_SEM rep(mem t,pc t,acc t,rtn t,iack t)))"
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:686: [ "Val3_CASES_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:687: [ "Val4Word4_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-688- [ "TamarackImp
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-949-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:950:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:951: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-952- SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1091-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1092:|- Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1093: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1094- SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1110- [],
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1111: "Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1112: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1113- SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1132-OK..
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1133:"Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1134: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1135- SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1173- NextState rep(ireq t,mem t,pc t,acc t,rtn t,iack t)"
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1174: [ "Val3_CASES_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1175: [ "Val4Word4_ASM rep" ]
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1176- [ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1213-goal proved
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1214:|- Val3_CASES_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex:1215: Val4Word4_ASM rep \(\wedge\)
hol88-2.02.19940316/Training/studies/microprocessor/verf.tex-1216- SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
##############################################
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex-309-\begintt
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex:310:let Val3_CASES_ASM = new_definition (
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex-311- `Val3_CASES_ASM`,
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex:312: "Val3_CASES_ASM (rep:^rep_ty) = \(\forall\)w. ((val3 rep) w) < 8");;
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex-313-
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex:314:let Val4Word4_ASM = new_definition (
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex-315- `Val4Word4_ASM`,
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex:316: "Val4Word4_ASM (rep:^rep_ty) =
hol88-2.02.19940316/Training/studies/microprocessor/abst.tex-317- \(\forall\)n. n < 16 ==> (((val4 rep) ((word4 rep) n)) = n)");;
##############################################
hol88-2.02.19940316/help/THEOREMS/axioms/create-axiom-doc-22- do map create_doc_file (axl) in
hol88-2.02.19940316/help/THEOREMS/axioms/create-axiom-doc:23: let ok = (new_theory \`dummy$$\`; new_parent \`$1\`; true) ? false in
hol88-2.02.19940316/help/THEOREMS/axioms/create-axiom-doc-24- print_string \`!!\`; print_newline();
hol88-2.02.19940316/help/THEOREMS/axioms/create-axiom-doc:25: ok => create_doc_files \`$1\` | print_string \`echo Failed\`;
hol88-2.02.19940316/help/THEOREMS/axioms/create-axiom-doc-26- print_newline(); print_string \`??\`; print_newline();
##############################################
hol88-2.02.19940316/help/ENTRIES/FIRST_ASSUM.doc-28-{
hol88-2.02.19940316/help/ENTRIES/FIRST_ASSUM.doc:29: FIRST_ASSUM (\asm. CONTR_TAC asm ORELSE ACCEPT_TAC asm)
hol88-2.02.19940316/help/ENTRIES/FIRST_ASSUM.doc-30-}
##############################################
hol88-2.02.19940316/help/ENTRIES/is_binder.doc-16-
hol88-2.02.19940316/help/ENTRIES/is_binder.doc:17:#is_binder `$?!`;;
hol88-2.02.19940316/help/ENTRIES/is_binder.doc-18-false : bool
##############################################
hol88-2.02.19940316/help/ENTRIES/is_constant.doc-20-
hol88-2.02.19940316/help/ENTRIES/is_constant.doc:21:#is_constant `$!`;;
hol88-2.02.19940316/help/ENTRIES/is_constant.doc-22-false : bool
##############################################
hol88-2.02.19940316/help/ENTRIES/is_infix.doc-13-{
hol88-2.02.19940316/help/ENTRIES/is_infix.doc:14:#is_infix `$+`;;
hol88-2.02.19940316/help/ENTRIES/is_infix.doc-15-false : bool
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-59- hol: basic-hol ${Theory}/HOL.th $(HolMl) lisp/banner.$(Obj) lisp/akcl.l
hol88-2.02.19940316/debian/patches/quilt-source-init:60:+# echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-61-+# 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-74-+# 'lisp `(setq %system-name "HOL")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:75:+# 'lisp `(setq %hol-dir "$(HOLdir)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:76:+# 'lisp `(setq %lib-dir "$(Library)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:77:+# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:78:+# 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-79-+# 'set_flag(`abort_when_fail`,false);;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:80:+# 'set_search_path[``; `~/`; `${Theory}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:81:+# 'set_help_search_path (words `$(Help)`);;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:82:+# 'set_library_search_path [`${Library}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-83-+# 'lisp `(setup)`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:84:+# 'save `${ExeName}`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-85-+# 'set_thm_count 0;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-87-+# | basic-hol
hol88-2.02.19940316/debian/patches/quilt-source-init:88: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-89- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-91-@@ -244,12 +272,8 @@ hol: basic-hol ${Theory}/HOL.th $(HolMl)
hol88-2.02.19940316/debian/patches/quilt-source-init:92: 'set_search_path[``; `~/`; `${Theory}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:93: 'set_help_search_path (words `$(Help)`);;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:94: 'set_library_search_path [`${Library}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-95-- 'lisp `(load "lisp/akcl.l")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-96-- 'lisp `(setup)`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:97:- 'save `${ExeName}`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-98-- 'set_thm_count 0;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-127- basic-hol: hol-lcf $(BasicHolLisp) ${Theory}/BASIC-HOL.th $(BasicHolMl)
hol88-2.02.19940316/debian/patches/quilt-source-init:128:+# echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-129-+# 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-145-+# 'activate_binders `bool`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:146:+# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:147:+# 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-148-+# 'lisp `(setq %system-name "BASIC-HOL")`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-152-+# | hol-lcf
hol88-2.02.19940316/debian/patches/quilt-source-init:153: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-154- 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-156-@@ -503,10 +553,8 @@ basic-hol: hol-lcf $(BasicHolLisp) ${The
hol88-2.02.19940316/debian/patches/quilt-source-init:157: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:158: 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-159- 'lisp `(setq %system-name "BASIC-HOL")`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-184-+# 'lisp `(setq %system-name "HOL-LCF")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:185:+# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-186-+# 'lisp `(setup)`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-195- 'lisp `(setq %system-name "HOL-LCF")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init:196: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/debian/patches/quilt-source-init-197-- 'lisp `(setup)`;;'\
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-15665-+#define MMcadar(x) (x)->c.c_car->c.c_cdr->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init:15666:+#define MMcaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init-15667-+#define MMcdaar(x) (x)->c.c_car->c.c_car->c.c_cdr
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-15673-+#define MMcaadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init:15674:+#define MMcaaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init-15675-+#define MMcadaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_car
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-15681-+#define MMcdadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/debian/patches/quilt-source-init:15682:+#define MMcdaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/debian/patches/quilt-source-init-15683-+#define MMcddaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_cdr
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16007-+object cadar();
hol88-2.02.19940316/debian/patches/quilt-source-init:16008:+object caddr();
hol88-2.02.19940316/debian/patches/quilt-source-init-16009-+object cdaar();
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16015-+object caadar();
hol88-2.02.19940316/debian/patches/quilt-source-init:16016:+object caaddr();
hol88-2.02.19940316/debian/patches/quilt-source-init-16017-+object cadaar();
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16023-+object cdadar();
hol88-2.02.19940316/debian/patches/quilt-source-init:16024:+object cdaddr();
hol88-2.02.19940316/debian/patches/quilt-source-init-16025-+object cddaar();
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16907-+#define Mcadar(x) (x)->c.c_car->c.c_cdr->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init:16908:+#define Mcaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init-16909-+#define Mcdaar(x) (x)->c.c_car->c.c_car->c.c_cdr
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16915-+#define Mcaadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init:16916:+#define Mcaaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init-16917-+#define Mcadaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_car
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16923-+#define Mcdadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/debian/patches/quilt-source-init:16924:+#define Mcdaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/debian/patches/quilt-source-init-16925-+#define Mcddaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_cdr
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16940-+#define CMPcadar(x) (x)->c.c_car->c.c_cdr->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init:16941:+#define CMPcaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init-16942-+#define CMPcdaar(x) (x)->c.c_car->c.c_car->c.c_cdr
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16948-+#define CMPcaadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init:16949:+#define CMPcaaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_car
hol88-2.02.19940316/debian/patches/quilt-source-init-16950-+#define CMPcadaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_car
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-16956-+#define CMPcdadar(x) (x)->c.c_car->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/debian/patches/quilt-source-init:16957:+#define CMPcdaddr(x) (x)->c.c_cdr->c.c_cdr->c.c_car->c.c_cdr
hol88-2.02.19940316/debian/patches/quilt-source-init-16958-+#define CMPcddaar(x) (x)->c.c_car->c.c_car->c.c_cdr->c.c_cdr
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-18558-+void Lcadadr(void);
hol88-2.02.19940316/debian/patches/quilt-source-init:18559:+void Lcaaddr(void);
hol88-2.02.19940316/debian/patches/quilt-source-init-18560-+void Lset_macro_character(void);
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-18671-+void Lcddadr(void);
hol88-2.02.19940316/debian/patches/quilt-source-init:18672:+void Lcdaddr(void);
hol88-2.02.19940316/debian/patches/quilt-source-init-18673-+void Lcadddr(void);
##############################################
hol88-2.02.19940316/debian/patches/quilt-source-init-18848-+void Lcdadr(void);
hol88-2.02.19940316/debian/patches/quilt-source-init:18849:+void Lcaddr(void);
hol88-2.02.19940316/debian/patches/quilt-source-init-18850-+void Lfmakunbound(void);
##############################################
hol88-2.02.19940316/debian/rules-46- for i in $$(find -maxdepth 1 -name "*hol*"); do \
hol88-2.02.19940316/debian/rules:47: printf 'install `'/usr/share/$(PD)'`;;\nlisp `(ml-save "foo")`;;\n' | ./$$i &&\
hol88-2.02.19940316/debian/rules-48- mv foo $$i; done
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-223-hol: basic-hol ${Theory}/HOL.th $(HolMl) lisp/banner.$(Obj) lisp/akcl.l
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:224: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-225- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-238- 'lisp `(setq %system-name "HOL")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:239: 'lisp `(setq %hol-dir "$(HOLdir)")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:240: 'lisp `(setq %lib-dir "$(Library)")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:241: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:242: 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-243- 'set_flag(`abort_when_fail`,false);;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:244: 'set_search_path[``; `~/`; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:245: 'set_help_search_path (words `$(Help)`);;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:246: 'set_library_search_path [`${Library}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-247- 'lisp `(load "lisp/akcl.l")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-248- 'lisp `(setup)`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:249: 'save `${ExeName}`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-250- 'set_thm_count 0;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-317-ml/tydefs_ml.o: basic-hol ${Theory}/HOL.th ml/load_thms.ml ml/tydefs.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:318: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-319- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-334-ml/tyfns_ml.o: basic-hol ${Theory}/HOL.th ml/prim_rec_ml.o ml/load_thms.ml ml/tyfns.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:335: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-336- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-342- ml/num.ml ml/numconv_ml.o
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:343: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-344- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-350- ml/numconv_ml.o ml/list.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:351: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-352- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-484-basic-hol: hol-lcf $(BasicHolLisp) ${Theory}/BASIC-HOL.th $(BasicHolMl)
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:485: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-486- 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-502- 'activate_binders `bool`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:503: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:504: 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-505- 'lisp `(setq %system-name "BASIC-HOL")`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-527- ml/hol-syn.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:528: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-529- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-543- ml/hol-syn_ml.o ml/hol-rule.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:544: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-545- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-551- ml/hol-syn_ml.o ml/hol-rule_ml.o ml/hol-drule.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:552: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-553- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-560- ml/drul.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:561: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-562- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-568- ml/hol-syn_ml.o ml/hol-thyfn.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:569: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-570- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-577- ml/drul_ml.o ml/tacticals.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:578: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-579- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-586- ml/drul_ml.o ml/tacticals_ml.o ml/tacont.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:587: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-588- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-596- ml/tactics.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:597: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-598- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-605- ml/drul_ml.o ml/tacticals_ml.o ml/conv.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:606: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-607- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-614- ml/hol-syn_ml.o ml/hol-net.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:615: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-616- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-624- ml/hol-net_ml.o ml/rewrite.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:625: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-626- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-634- ml/tactics_ml.o ml/conv_ml.o ml/resolve.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:635: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-636- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-643- ml/hol-drule_ml.o ml/drul_ml.o ml/tacticals_ml.o ml/goals.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:644: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-645- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-653- ml/goals_ml.o ml/stack.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:654: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-655- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-662- ml/hol-drule_ml.o ml/drul_ml.o ml/abs-rep.ml
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:663: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-664- 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-794- 'lisp `(setq %system-name "HOL-LCF")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile:795: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/quilt-source-init/Makefile-796- 'lisp `(setup)`;;'\
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-8672-\begin{verbatim}
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex:8673: FIRST_ASSUM (\asm. CONTR_TAC asm ORELSE ACCEPT_TAC asm)
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-8674-\end{verbatim}
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-11775-
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex:11776:#is_binder `$?!`;;
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-11777-false : bool
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-11937-
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex:11938:#is_constant `$!`;;
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-11939-false : bool
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-12158-\begin{verbatim}
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex:12159:#is_infix `$+`;;
hol88-2.02.19940316/.pc/quilt-source-init/Manual/Reference/entries.tex-12160-false : bool
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/lisp/f-cl.l-383-
hol88-2.02.19940316/.pc/quilt-source-init/lisp/f-cl.l:384:(defmacro cadaddr (x) `(car (cdaddr ,x)))
hol88-2.02.19940316/.pc/quilt-source-init/lisp/f-cl.l:385:(defmacro cadddaddr (x) `(caddr (cdaddr ,x)))
hol88-2.02.19940316/.pc/quilt-source-init/lisp/f-cl.l:386:(defmacro caddaddr (x) `(cadr (cdaddr ,x)))
hol88-2.02.19940316/.pc/quilt-source-init/lisp/f-cl.l:387:(defmacro caddadadr (x) `(caddr (cadadr ,x)))
hol88-2.02.19940316/.pc/quilt-source-init/lisp/f-cl.l-388-(defmacro cadadadr (x) `(cadr (cadadr ,x)))
##############################################
hol88-2.02.19940316/.pc/quilt-source-init/Library/res_quan/Manual/entries.tex-371-\begin{verbatim}
hol88-2.02.19940316/.pc/quilt-source-init/Library/res_quan/Manual/entries.tex:372: asm ?- Pk' ... asm ?- Pm' {asm,Pk',...,Pm'} ?- gl'
hol88-2.02.19940316/.pc/quilt-source-init/Library/res_quan/Manual/entries.tex-373-\end{verbatim}
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-223-hol: basic-hol ${Theory}/HOL.th $(HolMl) lisp/banner.$(Obj) lisp/akcl.l
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:224:# echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-225-# 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-238-# 'lisp `(setq %system-name "HOL")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:239:# 'lisp `(setq %hol-dir "$(HOLdir)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:240:# 'lisp `(setq %lib-dir "$(Library)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:241:# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:242:# 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-243-# 'set_flag(`abort_when_fail`,false);;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:244:# 'set_search_path[``; `~/`; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:245:# 'set_help_search_path (words `$(Help)`);;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:246:# 'set_library_search_path [`${Library}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-247-# 'lisp `(setup)`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:248:# 'save `${ExeName}`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-249-# 'set_thm_count 0;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-251-# | basic-hol
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:252: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-253- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-266- 'lisp `(setq %system-name "HOL")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:267: 'lisp `(setq %hol-dir "$(HOLdir)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:268: 'lisp `(setq %lib-dir "$(Library)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:269: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:270: 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-271- 'set_flag(`abort_when_fail`,false);;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:272: 'set_search_path[``; `~/`; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:273: 'set_help_search_path (words `$(Help)`);;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:274: 'set_library_search_path [`${Library}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-275- 'lisp `(setup)`;;' >foo2
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-342-ml/tydefs_ml.o: basic-hol ${Theory}/HOL.th ml/load_thms.ml ml/tydefs.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:343: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-344- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-359-ml/tyfns_ml.o: basic-hol ${Theory}/HOL.th ml/prim_rec_ml.o ml/load_thms.ml ml/tyfns.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:360: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-361- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-367- ml/num.ml ml/numconv_ml.o
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:368: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-369- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-375- ml/numconv_ml.o ml/list.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:376: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-377- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-509-basic-hol: hol-lcf $(BasicHolLisp) ${Theory}/BASIC-HOL.th $(BasicHolMl)
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:510:# echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-511-# 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-527-# 'activate_binders `bool`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:528:# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:529:# 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-530-# 'lisp `(setq %system-name "BASIC-HOL")`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-534-# | hol-lcf
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:535: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-536- 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-552- 'activate_binders `bool`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:553: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:554: 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-555- 'lisp `(setq %system-name "BASIC-HOL")`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-575- ml/hol-syn.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:576: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-577- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-591- ml/hol-syn_ml.o ml/hol-rule.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:592: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-593- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-599- ml/hol-syn_ml.o ml/hol-rule_ml.o ml/hol-drule.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:600: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-601- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-608- ml/drul.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:609: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-610- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-616- ml/hol-syn_ml.o ml/hol-thyfn.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:617: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-618- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-625- ml/drul_ml.o ml/tacticals.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:626: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-627- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-634- ml/drul_ml.o ml/tacticals_ml.o ml/tacont.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:635: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-636- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-644- ml/tactics.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:645: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-646- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-653- ml/drul_ml.o ml/tacticals_ml.o ml/conv.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:654: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-655- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-662- ml/hol-syn_ml.o ml/hol-net.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:663: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-664- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-672- ml/hol-net_ml.o ml/rewrite.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:673: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-674- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-682- ml/tactics_ml.o ml/conv_ml.o ml/resolve.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:683: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-684- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-691- ml/hol-drule_ml.o ml/drul_ml.o ml/tacticals_ml.o ml/goals.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:692: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-693- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-701- ml/goals_ml.o ml/stack.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:702: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-703- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-710- ml/hol-drule_ml.o ml/drul_ml.o ml/abs-rep.ml
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:711: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-712- 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-842-# 'lisp `(setq %system-name "HOL-LCF")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:843:# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-844-# 'lisp `(setup)`;;'\
##############################################
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-859- 'lisp `(setq %system-name "HOL-LCF")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile:860: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/.pc/FTBFS_detection_fix/Makefile-861- 'lisp `(setup)`;;' >foo
##############################################
hol88-2.02.19940316/Makefile-223-hol: basic-hol ${Theory}/HOL.th $(HolMl) lisp/banner.$(Obj) lisp/akcl.l
hol88-2.02.19940316/Makefile:224:# echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-225-# 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-238-# 'lisp `(setq %system-name "HOL")`;;'\
hol88-2.02.19940316/Makefile:239:# 'lisp `(setq %hol-dir "$(HOLdir)")`;;'\
hol88-2.02.19940316/Makefile:240:# 'lisp `(setq %lib-dir "$(Library)")`;;'\
hol88-2.02.19940316/Makefile:241:# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/Makefile:242:# 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/Makefile-243-# 'set_flag(`abort_when_fail`,false);;'\
hol88-2.02.19940316/Makefile:244:# 'set_search_path[``; `~/`; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile:245:# 'set_help_search_path (words `$(Help)`);;'\
hol88-2.02.19940316/Makefile:246:# 'set_library_search_path [`${Library}/`];;'\
hol88-2.02.19940316/Makefile-247-# 'lisp `(setup)`;;'\
hol88-2.02.19940316/Makefile:248:# 'save `${ExeName}`;;'\
hol88-2.02.19940316/Makefile-249-# 'set_thm_count 0;;'\
##############################################
hol88-2.02.19940316/Makefile-251-# | basic-hol
hol88-2.02.19940316/Makefile:252: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-253- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-266- 'lisp `(setq %system-name "HOL")`;;'\
hol88-2.02.19940316/Makefile:267: 'lisp `(setq %hol-dir "$(HOLdir)")`;;'\
hol88-2.02.19940316/Makefile:268: 'lisp `(setq %lib-dir "$(Library)")`;;'\
hol88-2.02.19940316/Makefile:269: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/Makefile:270: 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/Makefile-271- 'set_flag(`abort_when_fail`,false);;'\
hol88-2.02.19940316/Makefile:272: 'set_search_path[``; `~/`; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile:273: 'set_help_search_path (words `$(Help)`);;'\
hol88-2.02.19940316/Makefile:274: 'set_library_search_path [`${Library}/`];;'\
hol88-2.02.19940316/Makefile-275- 'lisp `(setup)`;;' >foo2
##############################################
hol88-2.02.19940316/Makefile-346-ml/tydefs_ml.o: basic-hol ${Theory}/HOL.th ml/load_thms.ml ml/tydefs.ml
hol88-2.02.19940316/Makefile:347: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-348- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-363-ml/tyfns_ml.o: basic-hol ${Theory}/HOL.th ml/prim_rec_ml.o ml/load_thms.ml ml/tyfns.ml
hol88-2.02.19940316/Makefile:364: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-365- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-371- ml/num.ml ml/numconv_ml.o
hol88-2.02.19940316/Makefile:372: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-373- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-379- ml/numconv_ml.o ml/list.ml
hol88-2.02.19940316/Makefile:380: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-381- 'load_theory `HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-513-basic-hol: hol-lcf $(BasicHolLisp) ${Theory}/BASIC-HOL.th $(BasicHolMl)
hol88-2.02.19940316/Makefile:514:# echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-515-# 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-531-# 'activate_binders `bool`;;'\
hol88-2.02.19940316/Makefile:532:# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/Makefile:533:# 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/Makefile-534-# 'lisp `(setq %system-name "BASIC-HOL")`;;'\
##############################################
hol88-2.02.19940316/Makefile-538-# | hol-lcf
hol88-2.02.19940316/Makefile:539: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-540- 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-556- 'activate_binders `bool`;;'\
hol88-2.02.19940316/Makefile:557: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/Makefile:558: 'lisp `(setq %version "$(Version)")`;;'\
hol88-2.02.19940316/Makefile-559- 'lisp `(setq %system-name "BASIC-HOL")`;;'\
##############################################
hol88-2.02.19940316/Makefile-579- ml/hol-syn.ml
hol88-2.02.19940316/Makefile:580: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-581- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-595- ml/hol-syn_ml.o ml/hol-rule.ml
hol88-2.02.19940316/Makefile:596: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-597- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-603- ml/hol-syn_ml.o ml/hol-rule_ml.o ml/hol-drule.ml
hol88-2.02.19940316/Makefile:604: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-605- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-612- ml/drul.ml
hol88-2.02.19940316/Makefile:613: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-614- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-620- ml/hol-syn_ml.o ml/hol-thyfn.ml
hol88-2.02.19940316/Makefile:621: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-622- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-629- ml/drul_ml.o ml/tacticals.ml
hol88-2.02.19940316/Makefile:630: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-631- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-638- ml/drul_ml.o ml/tacticals_ml.o ml/tacont.ml
hol88-2.02.19940316/Makefile:639: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-640- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-648- ml/tactics.ml
hol88-2.02.19940316/Makefile:649: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-650- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-657- ml/drul_ml.o ml/tacticals_ml.o ml/conv.ml
hol88-2.02.19940316/Makefile:658: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-659- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-666- ml/hol-syn_ml.o ml/hol-net.ml
hol88-2.02.19940316/Makefile:667: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-668- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-676- ml/hol-net_ml.o ml/rewrite.ml
hol88-2.02.19940316/Makefile:677: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-678- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-686- ml/tactics_ml.o ml/conv_ml.o ml/resolve.ml
hol88-2.02.19940316/Makefile:687: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-688- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-695- ml/hol-drule_ml.o ml/drul_ml.o ml/tacticals_ml.o ml/goals.ml
hol88-2.02.19940316/Makefile:696: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-697- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-705- ml/goals_ml.o ml/stack.ml
hol88-2.02.19940316/Makefile:706: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-707- 'load_theory `bool`;;'\
##############################################
hol88-2.02.19940316/Makefile-714- ml/hol-drule_ml.o ml/drul_ml.o ml/abs-rep.ml
hol88-2.02.19940316/Makefile:715: echo 'set_search_path[``; `${Theory}/`];;'\
hol88-2.02.19940316/Makefile-716- 'load_theory `BASIC-HOL`;;'\
##############################################
hol88-2.02.19940316/Makefile-846-# 'lisp `(setq %system-name "HOL-LCF")`;;'\
hol88-2.02.19940316/Makefile:847:# 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/Makefile-848-# 'lisp `(setup)`;;'\
##############################################
hol88-2.02.19940316/Makefile-863- 'lisp `(setq %system-name "HOL-LCF")`;;'\
hol88-2.02.19940316/Makefile:864: 'lisp `(setq %liszt "$(LisztComm)")`;;'\
hol88-2.02.19940316/Makefile-865- 'lisp `(setup)`;;' >foo