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 10034 4bca6b2d2589
parent 10004 0b8fc904c70b
child 10412 1a1b4c1b2b7c 
--- a/src/Provers/simplifier.ML	Tue Sep 19 23:52:37 2000 +0200
+++ b/src/Provers/simplifier.ML	Tue Sep 19 23:53:00 2000 +0200
@@ -518,19 +518,19 @@
 
 val cong_modifiers =
  [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
-  Args.$$$ congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local)];
+  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
+  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
 
 val simp_modifiers =
  [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
+  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
+  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    @ cong_modifiers;
 
 val simp_modifiers' =
- [Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
+ [Args.add -- Args.colon >> K (I, simp_add_local),
+  Args.del -- Args.colon >> K (I, simp_del_local),
   Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    @ cong_modifiers;
isabelle