added simplification meta rules;
authorwenzelm
Wed, 23 Jul 1997 16:03:19 +0200
changeset 3567 e2539e1980b4
parent 3566 c9c351374651
child 3568 36ff1ab12021
added simplification meta rules;
NEWS
--- a/NEWS	Wed Jul 23 12:54:49 1997 +0200
+++ b/NEWS	Wed Jul 23 16:03:19 1997 +0200
@@ -14,7 +14,10 @@
 * improved output of warnings / errors;
 
 * deleted the obsolete tactical STATE, which was declared by
-	fun STATE tacfun st = tacfun st st;
+    fun STATE tacfun st = tacfun st st;
+
+* added simplification meta rules
+    (asm_)(full_)simplify: simpset -> thm -> thm;
 
 
 New in Isabelle94-8 (May 1997)