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.
Set.insert with authentic syntax
authorhaftmann
Fri, 05 Jun 2009 08:00:53 +0200
changeset 31460 d97fa41cc600
parent 31459 ae39b7b2a68a
child 31461 d54b743b52a3
Set.insert with authentic syntax
src/HOL/TLA/Intensional.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/TLA/Intensional.thy	Thu Jun 04 16:55:20 2009 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Jun 05 08:00:53 2009 +0200
@@ -126,8 +126,8 @@
   "_liftLeq"      == "_lift2 (op <=)"
   "_liftMem"      == "_lift2 (op :)"
   "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
-  "_liftFinset (_liftargs x xs)"  == "_lift2 insert x (_liftFinset xs)"
-  "_liftFinset x" == "_lift2 insert x (_const {})"
+  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
+  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
   "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
   "_liftPair"     == "_lift2 Pair"
   "_liftCons"     == "lift2 Cons"
isabelle