--- a/src/HOL/HOLCF/Porder.thy Fri Jun 26 10:20:33 2015 +0200
+++ b/src/HOL/HOLCF/Porder.thy Fri Jun 26 11:07:04 2015 +0200
@@ -126,7 +126,7 @@
"LUB n. t n == lub (range t)"
notation (xsymbols)
- Lub (binder "\<Squnion> " 10)
+ Lub (binder "\<Squnion>" 10)
text {* access to some definition as inference rule *}
--- a/src/HOL/Set_Interval.thy Fri Jun 26 10:20:33 2015 +0200
+++ b/src/HOL/Set_Interval.thy Fri Jun 26 11:07:04 2015 +0200
@@ -66,10 +66,10 @@
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)
syntax (xsymbols)
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
syntax (latex output)
"_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
--- a/src/HOL/UNITY/Union.thy Fri Jun 26 10:20:33 2015 +0200
+++ b/src/HOL/UNITY/Union.thy Fri Jun 26 11:07:04 2015 +0200
@@ -47,8 +47,8 @@
"_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)
+ "_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)"