# HG changeset patch
# User berghofe
# Date 835356895 -7200
# Node ID bc506bcb9fe45508951971261dcd33f412cd31ca
# Parent  e381e1c51689b62fe94eff4044b95cd03fa19e3c
Added function Addss.

diff -r e381e1c51689 -r bc506bcb9fe4 src/HOL/simpdata.ML
--- 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", []),