equal
deleted
inserted
replaced
19 sig |
19 sig |
20 include THM |
20 include THM |
21 structure Ctermtab: TABLE |
21 structure Ctermtab: TABLE |
22 structure Thmtab: TABLE |
22 structure Thmtab: TABLE |
23 val aconvc: cterm * cterm -> bool |
23 val aconvc: cterm * cterm -> bool |
24 val add_cterm_frees: cterm -> cterm list -> cterm list |
24 val add_frees: thm -> cterm list -> cterm list |
|
25 val add_vars: thm -> cterm list -> cterm list |
25 val all_name: string * cterm -> cterm -> cterm |
26 val all_name: string * cterm -> cterm -> cterm |
26 val all: cterm -> cterm -> cterm |
27 val all: cterm -> cterm -> cterm |
27 val mk_binop: cterm -> cterm -> cterm -> cterm |
28 val mk_binop: cterm -> cterm -> cterm -> cterm |
28 val dest_binop: cterm -> cterm * cterm |
29 val dest_binop: cterm -> cterm * cterm |
29 val dest_implies: cterm -> cterm * cterm |
30 val dest_implies: cterm -> cterm * cterm |
110 |
111 |
111 (* collecting cterms *) |
112 (* collecting cterms *) |
112 |
113 |
113 val op aconvc = op aconv o apply2 Thm.term_of; |
114 val op aconvc = op aconv o apply2 Thm.term_of; |
114 |
115 |
115 fun add_cterm_frees ct = |
116 val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); |
116 let |
117 val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); |
117 val thy = Thm.theory_of_cterm ct; |
|
118 val t = Thm.term_of ct; |
|
119 in |
|
120 Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t |
|
121 end; |
|
122 |
118 |
123 |
119 |
124 (* cterm constructors and destructors *) |
120 (* cterm constructors and destructors *) |
125 |
121 |
126 fun all_name (x, t) A = |
122 fun all_name (x, t) A = |