| changeset 1821 | bc506bcb9fe4 |
| parent 1758 | 60613b065e9b |
| child 1874 | 35f22792aade |
--- a/src/HOL/simpdata.ML Fri Jun 21 12:18:50 1996 +0200 +++ b/src/HOL/simpdata.ML Fri Jun 21 13:34:55 1996 +0200 @@ -104,6 +104,8 @@ infix 4 addss; fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; +fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1); + val mksimps_pairs = [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), ("All", [spec]), ("True", []), ("False", []),