equal
deleted
inserted
replaced
106 (*not totally safe: may instantiate unknowns that appear also in other subgoals*) |
106 (*not totally safe: may instantiate unknowns that appear also in other subgoals*) |
107 val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true,true,true); |
107 val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true,true,true); |
108 |
108 |
109 (*Add a simpset to a classical set!*) |
109 (*Add a simpset to a classical set!*) |
110 (*Caution: only one simpset added can be added by each of addSss and addss*) |
110 (*Caution: only one simpset added can be added by each of addSss and addss*) |
111 fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac", |
111 fun cs addSss ss = Classical.addSafter (cs, ("safe_asm_full_simp_tac", |
112 CHANGED o safe_asm_full_simp_tac ss)); |
112 CHANGED o safe_asm_full_simp_tac ss)); |
113 fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
113 fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
114 CHANGED o Simplifier.asm_full_simp_tac ss)); |
114 CHANGED o Simplifier.asm_full_simp_tac ss)); |
115 |
115 |
116 |
116 |