equal
deleted
inserted
replaced
45 ------- |
45 ------- |
46 A ==> B |
46 A ==> B |
47 *) |
47 *) |
48 fun presume_export _ = assume_export false; |
48 fun presume_export _ = assume_export false; |
49 |
49 |
50 val assume = norm_hhf o Thm.assume; |
50 val assume = MetaSimplifier.norm_hhf o Thm.assume; |
51 |
51 |
52 |
52 |
53 |
53 |
54 (** local context data **) |
54 (** local context data **) |
55 |
55 |
98 |
98 |
99 (* export *) |
99 (* export *) |
100 |
100 |
101 fun export is_goal inner outer = |
101 fun export is_goal inner outer = |
102 let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in |
102 let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in |
103 norm_hhf_protect |
103 MetaSimplifier.norm_hhf_protect |
104 #> fold_rev (fn (e, As) => e is_goal As) asms |
104 #> fold_rev (fn (e, As) => e is_goal As) asms |
105 #> norm_hhf_protect |
105 #> MetaSimplifier.norm_hhf_protect |
106 end; |
106 end; |
107 |
107 |
108 fun export_morphism inner outer = |
108 fun export_morphism inner outer = |
109 let |
109 let |
110 val thm = export false inner outer; |
110 val thm = export false inner outer; |