src/Provers/clasimp.ML
changeset 9952 24914e42b857
parent 9893 93d2fde0306c
child 10033 fc4e7432b2b1
     1.1 --- a/src/Provers/clasimp.ML	Wed Sep 13 22:29:37 2000 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Wed Sep 13 22:31:19 2000 +0200
     1.3 @@ -272,13 +272,11 @@
     1.4  (* method modifiers *)
     1.5  
     1.6  val iffN = "iff";
     1.7 -val addN = "add";
     1.8 -val delN = "del";
     1.9  
    1.10  val iff_modifiers =
    1.11   [Args.$$$ iffN -- Args.colon >> K ((I, iff_add_local): Method.modifier),
    1.12 -  Args.$$$ iffN -- Args.$$$ addN -- Args.colon >> K (I, iff_add_local),
    1.13 -  Args.$$$ iffN -- Args.$$$ delN -- Args.colon >> K (I, iff_del_local)];
    1.14 +  Args.$$$ iffN -- Args.$$$ Args.addN -- Args.colon >> K (I, iff_add_local),
    1.15 +  Args.$$$ iffN -- Args.$$$ Args.delN -- Args.colon >> K (I, iff_del_local)];
    1.16  
    1.17  val clasimp_modifiers =
    1.18    Simplifier.simp_modifiers @ Splitter.split_modifiers @