===========================================================
                                      .___ __  __   
          _________________  __ __  __| _/|__|/  |_ 
         / ___\_` __ \__  \ |  |  \/ __ | | \\_  __\
        / /_/  >  | \// __ \|  |  / /_/ | |  ||  |  
        \___  /|__|  (____  /____/\____ | |__||__|  
       /_____/            \/           \/           
              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