Set.insert with authentic syntax
authorhaftmann
Fri Jun 05 08:00:53 2009 +0200 (2009-06-05)
changeset 31460d97fa41cc600
parent 31459 ae39b7b2a68a
child 31461 d54b743b52a3
Set.insert with authentic syntax
src/HOL/TLA/Intensional.thy
     1.1 --- a/src/HOL/TLA/Intensional.thy	Thu Jun 04 16:55:20 2009 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Jun 05 08:00:53 2009 +0200
     1.3 @@ -126,8 +126,8 @@
     1.4    "_liftLeq"      == "_lift2 (op <=)"
     1.5    "_liftMem"      == "_lift2 (op :)"
     1.6    "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
     1.7 -  "_liftFinset (_liftargs x xs)"  == "_lift2 insert x (_liftFinset xs)"
     1.8 -  "_liftFinset x" == "_lift2 insert x (_const {})"
     1.9 +  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
    1.10 +  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
    1.11    "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
    1.12    "_liftPair"     == "_lift2 Pair"
    1.13    "_liftCons"     == "lift2 Cons"