# HG changeset patch
# User wenzelm
# Date 949152136 -3600
# Node ID 4b9451fae406a7ff8bc362331809037b2902b658
# Parent  77b3bc101de51068b26937e5d786a1da97d04dcc
simp_all method;

diff -r 77b3bc101de5 -r 4b9451fae406 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Jan 28 21:58:39 2000 +0100
+++ b/src/Provers/simplifier.ML	Sat Jan 29 14:22:16 2000 +0100
@@ -487,6 +487,11 @@
 
 fun simp_method tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>
+    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_simpset ctxt)))
+  |> Method.bang_sectioned_args simp_modifiers';
+
+fun simp_method' tac =
+  (fn prems => fn ctxt => Method.METHOD (fn facts =>
     HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
   |> Method.bang_sectioned_args simp_modifiers';
   
@@ -494,12 +499,14 @@
 (* setup_methods *)
 
 val setup_methods = Method.add_methods
- [(simpN,               simp_method (CHANGED oo asm_full_simp_tac), "full simplification"),
-  ("simp_tac",          simp_method simp_tac, "simp_tac (improper!)"),
-  ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac (improper!)"),
-  ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac (improper!)"),
-  ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
-  ("asm_lr_simp_tac",   simp_method asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
+ [(simpN,               simp_method' (CHANGED oo asm_full_simp_tac), "full simplification"),
+  ("simp_all",          simp_method  (CHANGED o ALLGOALS o asm_full_simp_tac),
+    "full simplification (all goals)"),
+  ("simp_tac",          simp_method' simp_tac, "simp_tac (improper!)"),
+  ("asm_simp_tac",      simp_method' asm_simp_tac, "asm_simp_tac (improper!)"),
+  ("full_simp_tac",     simp_method' full_simp_tac, "full_simp_tac (improper!)"),
+  ("asm_full_simp_tac", simp_method' asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
+  ("asm_lr_simp_tac",   simp_method' asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];