src/HOL/simpdata.ML
changeset 1821 bc506bcb9fe4
parent 1758 60613b065e9b
child 1874 35f22792aade
equal deleted inserted replaced
1820:e381e1c51689 1821:bc506bcb9fe4
   102 
   102 
   103 (*Add a simpset to a classical set!*)
   103 (*Add a simpset to a classical set!*)
   104 infix 4 addss;
   104 infix 4 addss;
   105 fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
   105 fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
   106 
   106 
       
   107 fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1);
       
   108 
   107 val mksimps_pairs =
   109 val mksimps_pairs =
   108   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   110   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   109    ("All", [spec]), ("True", []), ("False", []),
   111    ("All", [spec]), ("True", []), ("False", []),
   110    ("If", [if_bool_eq RS iffD1])];
   112    ("If", [if_bool_eq RS iffD1])];
   111 
   113