# HG changeset patch
# User oheimb
# Date 830272283 -7200
# Node ID db29ab9c14905687a407876e892cdbf50961e31c
# Parent  36ba4da350c34df12b21bee261542fe8ef65a20a
*** empty log message ***

diff -r 36ba4da350c3 -r db29ab9c1490 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Apr 23 17:04:23 1996 +0200
+++ b/src/Provers/simplifier.ML	Tue Apr 23 17:11:23 1996 +0200
@@ -17,7 +17,8 @@
   val addsimps: simpset * thm list -> simpset
   val delsimps: simpset * thm list -> simpset
   val asm_full_simp_tac: simpset -> int -> tactic
-  val asm_simp_tac: simpset -> int -> tactic
+  val     full_simp_tac: simpset -> int -> tactic
+  val      asm_simp_tac: simpset -> int -> tactic
   val empty_ss: simpset
   val merge_ss: simpset * simpset -> simpset
   val prems_of_ss: simpset -> thm list
@@ -32,7 +33,8 @@
   val Addsimps: thm list -> unit
   val Delsimps: thm list -> unit
   val Simp_tac: int -> tactic
-  val Asm_simp_tac: int -> tactic
+  val      Asm_simp_tac: int -> tactic
+  val     Full_simp_tac: int -> tactic
   val Asm_full_simp_tac: int -> tactic
 end;
 
@@ -165,12 +167,14 @@
       and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
   in simp_loop_tac end;
 
-val asm_full_simp_tac = gen_simp_tac (true,true);
-val asm_simp_tac = gen_simp_tac (false,true);
-val simp_tac = gen_simp_tac (false,false);
+val asm_full_simp_tac = gen_simp_tac (true ,true );
+val     full_simp_tac = gen_simp_tac (true ,false);
+val      asm_simp_tac = gen_simp_tac (false,true );
+val          simp_tac = gen_simp_tac (false,false);
 
 fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i;
-fun Asm_simp_tac i = asm_simp_tac (!simpset) i;
-fun Simp_tac i = simp_tac (!simpset) i;
+fun     Full_simp_tac i =     full_simp_tac (!simpset) i;
+fun      Asm_simp_tac i =      asm_simp_tac (!simpset) i;
+fun          Simp_tac i =          simp_tac (!simpset) i;
 
 end;