equal
deleted
inserted
replaced
119 val goal = Logic.mk_implies |
119 val goal = Logic.mk_implies |
120 (if conclusion then (orig, reordered) else (reordered, orig)); |
120 (if conclusion then (orig, reordered) else (reordered, orig)); |
121 |
121 |
122 (* simp add: sep_conj_ac *) |
122 (* simp add: sep_conj_ac *) |
123 val sep_conj_ac_tac = Simplifier.asm_full_simp_tac |
123 val sep_conj_ac_tac = Simplifier.asm_full_simp_tac |
124 (put_simpset HOL_basic_ss ctxt addsimps SepConj.sep_conj_ac); |
124 (HOL_basic_ss addsimps SepConj.sep_conj_ac); |
125 |
125 |
126 in |
126 in |
127 (* XXX: normally you'd want to keep track of what variables we want to make |
127 (* XXX: normally you'd want to keep track of what variables we want to make |
128 schematic and which ones are bound, but we don't use fixed names for |
128 schematic and which ones are bound, but we don't use fixed names for |
129 the rules we make, so we use Drule.export_without_context to schematise |
129 the rules we make, so we use Drule.export_without_context to schematise |