changeset 30304 | d8e4cd2ac2a1 |
parent 16977 | 7c04742abac3 |
child 32960 | 69916a850301 |
--- a/src/HOL/UNITY/Union.thy Thu Mar 05 08:23:10 2009 +0100 +++ b/src/HOL/UNITY/Union.thy Thu Mar 05 08:23:11 2009 +0100 @@ -43,7 +43,7 @@ translations "JN x : A. B" == "JOIN A (%x. B)" "JN x y. B" == "JN x. JN y. B" - "JN x. B" == "JOIN UNIV (%x. B)" + "JN x. B" == "JOIN CONST UNIV (%x. B)" syntax (xsymbols) SKIP :: "'a program" ("\<bottom>")