Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
standard congs;
authorwenzelm
Wed, 23 Jul 1997 12:54:49 +0200
changeset 3566 c9c351374651
parent 3565 c64410e701fb
child 3567 e2539e1980b4
standard congs;
src/FOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/simpdata.ML	Wed Jul 23 11:54:32 1997 +0200
+++ b/src/FOL/simpdata.ML	Wed Jul 23 12:54:49 1997 +0200
@@ -190,9 +190,9 @@
 (*Add congruence rules for = or <-> (instead of ==) *)
 infix 4 addcongs delcongs;
 fun ss addcongs congs =
-        ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
 fun ss delcongs congs =
-        ss deleqcongs (congs RL [eq_reflection,iff_reflection]);
+        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
 
 fun Addcongs congs = (simpset := !simpset addcongs congs);
 fun Delcongs congs = (simpset := !simpset delcongs congs);
isabelle