equal
deleted
inserted
replaced
72 fun expand defs = |
72 fun expand defs = |
73 Drule.implies_intr_list defs |
73 Drule.implies_intr_list defs |
74 #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs) |
74 #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs) |
75 #> funpow (length defs) (fn th => Drule.reflexive_thm RS th); |
75 #> funpow (length defs) (fn th => Drule.reflexive_thm RS th); |
76 |
76 |
77 fun expand_term defs = |
77 val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of); |
78 let |
|
79 val eqs = defs |> map (Thm.term_of #> abs_def #> (fn ((x, U), u) => (x, (U, u)))); |
|
80 fun get_def (Free (x, _)) = AList.lookup (op =) eqs x |
|
81 | get_def _ = NONE; |
|
82 in Envir.expand_term get_def end; |
|
83 |
78 |
84 fun def_export _ defs = (expand defs, expand_term defs); |
79 fun def_export _ defs = (expand defs, expand_term defs); |
85 |
80 |
86 |
81 |
87 (* add defs *) |
82 (* add defs *) |