src/Provers/clasimp.ML
changeset 9952 24914e42b857
parent 9893 93d2fde0306c
child 10033 fc4e7432b2b1
--- a/src/Provers/clasimp.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Provers/clasimp.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -272,13 +272,11 @@
 (* method modifiers *)
 
 val iffN = "iff";
-val addN = "add";
-val delN = "del";
 
 val iff_modifiers =
  [Args.$$$ iffN -- Args.colon >> K ((I, iff_add_local): Method.modifier),
-  Args.$$$ iffN -- Args.$$$ addN -- Args.colon >> K (I, iff_add_local),
-  Args.$$$ iffN -- Args.$$$ delN -- Args.colon >> K (I, iff_del_local)];
+  Args.$$$ iffN -- Args.$$$ Args.addN -- Args.colon >> K (I, iff_add_local),
+  Args.$$$ iffN -- Args.$$$ Args.delN -- Args.colon >> K (I, iff_del_local)];
 
 val clasimp_modifiers =
   Simplifier.simp_modifiers @ Splitter.split_modifiers @