124 FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), |
124 FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), |
125 eq_assume_tac, ematch_tac @{thms FalseE}]; |
125 eq_assume_tac, ematch_tac @{thms FalseE}]; |
126 |
126 |
127 val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
127 val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
128 |
128 |
129 structure SplitterData = |
129 structure Splitter = Splitter |
130 struct |
130 ( |
131 structure Simplifier = Simplifier |
131 val thy = @{theory} |
132 val mk_eq = mk_eq |
132 val mk_eq = mk_eq |
133 val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} |
133 val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} |
134 val iffD = @{thm iffD2} |
134 val iffD = @{thm iffD2} |
135 val disjE = @{thm disjE} |
135 val disjE = @{thm disjE} |
136 val conjE = @{thm conjE} |
136 val conjE = @{thm conjE} |
137 val exE = @{thm exE} |
137 val exE = @{thm exE} |
138 val contrapos = @{thm contrapos_nn} |
138 val contrapos = @{thm contrapos_nn} |
139 val contrapos2 = @{thm contrapos_pp} |
139 val contrapos2 = @{thm contrapos_pp} |
140 val notnotD = @{thm notnotD} |
140 val notnotD = @{thm notnotD} |
141 end; |
141 ); |
142 |
142 |
143 structure Splitter = SplitterFun(SplitterData); |
143 val split_tac = Splitter.split_tac; |
144 |
|
145 val split_tac = Splitter.split_tac; |
|
146 val split_inside_tac = Splitter.split_inside_tac; |
144 val split_inside_tac = Splitter.split_inside_tac; |
147 |
145 |
148 val op addsplits = Splitter.addsplits; |
146 val op addsplits = Splitter.addsplits; |
149 val op delsplits = Splitter.delsplits; |
147 val op delsplits = Splitter.delsplits; |
150 |
148 |
151 |
149 |
152 (* integration of simplifier with classical reasoner *) |
150 (* integration of simplifier with classical reasoner *) |
153 |
151 |
154 structure Clasimp = ClasimpFun |
152 structure Clasimp = ClasimpFun |