equal
deleted
inserted
replaced
46 ------- |
46 ------- |
47 A ==> B |
47 A ==> B |
48 *) |
48 *) |
49 fun presume_export _ = assume_export false; |
49 fun presume_export _ = assume_export false; |
50 |
50 |
51 val assume = MetaSimplifier.norm_hhf o Thm.assume; |
51 val assume = Raw_Simplifier.norm_hhf o Thm.assume; |
52 |
52 |
53 |
53 |
54 |
54 |
55 (** local context data **) |
55 (** local context data **) |
56 |
56 |
108 |
108 |
109 |
109 |
110 (* export *) |
110 (* export *) |
111 |
111 |
112 fun export is_goal inner outer = |
112 fun export is_goal inner outer = |
113 MetaSimplifier.norm_hhf_protect #> |
113 Raw_Simplifier.norm_hhf_protect #> |
114 fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> |
114 fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> |
115 MetaSimplifier.norm_hhf_protect; |
115 Raw_Simplifier.norm_hhf_protect; |
116 |
116 |
117 fun export_term inner outer = |
117 fun export_term inner outer = |
118 fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); |
118 fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); |
119 |
119 |
120 fun export_morphism inner outer = |
120 fun export_morphism inner outer = |