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 [])"