--- a/src/HOL/UNITY/Union.thy Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOL/UNITY/Union.thy Tue Mar 02 23:59:54 2010 +0100
@@ -35,21 +35,22 @@
safety_prop :: "'a program set => bool"
"safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
+notation
+ SKIP ("\<bottom>") and
+ Join (infixl "\<squnion>" 65)
+
syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
+syntax (xsymbols)
+ "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
translations
"JN x: A. B" == "CONST JOIN A (%x. B)"
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
-syntax (xsymbols)
- SKIP :: "'a program" ("\<bottom>")
- Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
- "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
- "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
-
subsection{*SKIP*}