Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/simplifier.ML
changeset 10004 0b8fc904c70b
parent 9952 24914e42b857
child 10034 4bca6b2d2589 
--- a/src/Provers/simplifier.ML	Fri Sep 15 21:49:54 2000 +0200
+++ b/src/Provers/simplifier.ML	Fri Sep 15 21:52:09 2000 +0200
@@ -67,6 +67,7 @@
   val Addcongs: thm list -> unit
   val Delcongs: thm list -> unit
   val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
+  val safe_asm_full_simp_tac: simpset -> int -> tactic
   val               simp_tac: simpset -> int -> tactic
   val           asm_simp_tac: simpset -> int -> tactic
   val          full_simp_tac: simpset -> int -> tactic
@@ -414,11 +415,12 @@
               TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
     in simp_loop_tac end;
 
-val          simp_tac = generic_simp_tac false (false, false, false);
-val      asm_simp_tac = generic_simp_tac false (false, true, false);
-val     full_simp_tac = generic_simp_tac false (true,  false, false);
-val   asm_lr_simp_tac = generic_simp_tac false (true,  true, false);
-val asm_full_simp_tac = generic_simp_tac false (true,  true, true);
+val simp_tac = generic_simp_tac false (false, false, false);
+val asm_simp_tac = generic_simp_tac false (false, true, false);
+val full_simp_tac = generic_simp_tac false (true, false, false);
+val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
+val asm_full_simp_tac = generic_simp_tac false (true, true, true);
+val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
 
 
 (*the abstraction over the proof state delays the dereferencing*)
isabelle