equal
deleted
inserted
replaced
87 ----------- |
87 ----------- |
88 B a |
88 B a |
89 *) |
89 *) |
90 fun expand defs = |
90 fun expand defs = |
91 Drule.implies_intr_list defs |
91 Drule.implies_intr_list defs |
92 #> Drule.generalize ([], map (#1 o head_of_def o Thm.term_of) defs) |
92 #> Drule.generalize |
|
93 (Symtab.empty, fold (Symtab.insert_set o #1 o head_of_def o Thm.term_of) defs Symtab.empty) |
93 #> funpow (length defs) (fn th => Drule.reflexive_thm RS th); |
94 #> funpow (length defs) (fn th => Drule.reflexive_thm RS th); |
94 |
95 |
95 val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of); |
96 val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of); |
96 |
97 |
97 fun def_export _ defs = (expand defs, expand_term defs); |
98 fun def_export _ defs = (expand defs, expand_term defs); |