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.
tuned congs: standard;
authorwenzelm
Wed, 23 Jul 1997 11:07:36 +0200
changeset 3559 7a176613e5d5
parent 3558 258eee1a056e
child 3560 7db9a44dfa06
tuned congs: standard;
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/simpdata.ML	Wed Jul 23 11:04:19 1997 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 23 11:07:36 1997 +0200
@@ -108,8 +108,8 @@
 
 (*Add congruence rules for = (instead of ==) *)
 infix 4 addcongs delcongs;
-fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
-fun ss delcongs congs = ss deleqcongs (congs RL [eq_reflection]);
+fun ss addcongs congs = ss addeqcongs (map standard (congs RL [eq_reflection]));
+fun ss delcongs congs = ss deleqcongs (map standard (congs RL [eq_reflection]));
 
 fun Addcongs congs = (simpset := !simpset addcongs congs);
 fun Delcongs congs = (simpset := !simpset delcongs congs);
isabelle