src/Provers/simplifier.ML
changeset 7132 5c31d06ead04
parent 6994 f22a51ed9f11
child 7177 6bb7ad30f3da
--- a/src/Provers/simplifier.ML	Fri Jul 30 13:42:57 1999 +0200
+++ b/src/Provers/simplifier.ML	Fri Jul 30 13:43:26 1999 +0200
@@ -477,11 +477,11 @@
  [(simpN,               simp_method true true asm_full_simp_tac, "simplification"),
   (asm_simpN,           simp_method false true asm_full_simp_tac,
     "simplification (including assumption)"),
-  ("simp_tac",          simp_method false false simp_tac, "simp_tac"),
-  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac"),
-  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac"),
-  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac"),
-  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac")];
+  ("simp_tac",          simp_method false false simp_tac, "simp_tac (improper!)"),
+  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"),
+  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac (improper!)"),
+  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
+  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];