equal
deleted
inserted
replaced
41 "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) |
41 "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) |
42 |
42 |
43 translations |
43 translations |
44 "JN x : A. B" == "JOIN A (%x. B)" |
44 "JN x : A. B" == "JOIN A (%x. B)" |
45 "JN x y. B" == "JN x. JN y. B" |
45 "JN x y. B" == "JN x. JN y. B" |
46 "JN x. B" == "JOIN UNIV (%x. B)" |
46 "JN x. B" == "JOIN CONST UNIV (%x. B)" |
47 |
47 |
48 syntax (xsymbols) |
48 syntax (xsymbols) |
49 SKIP :: "'a program" ("\<bottom>") |
49 SKIP :: "'a program" ("\<bottom>") |
50 Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65) |
50 Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65) |
51 "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10) |
51 "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10) |