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 @