src/HOL/TLA/Intensional.thy
changeset 7224 e41e64476f9b
parent 6340 7d5cbd5819a0
child 9517 f58863b1406a
     1.1 --- a/src/HOL/TLA/Intensional.thy	Mon Aug 16 22:04:07 1999 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Aug 16 22:07:12 1999 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4    "_liftFinset x" == "_lift2 insert x (_const {})"
     1.5    "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
     1.6    "_liftPair"     == "_lift2 Pair"
     1.7 -  "_liftCons"     == "lift2 (op #)"
     1.8 +  "_liftCons"     == "lift2 Cons"
     1.9    "_liftApp"      == "lift2 (op @)"
    1.10    "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
    1.11    "_liftList x"   == "_liftCons x (_const [])"