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