# HG changeset patch
# User huffman
# Date 1133308524 -3600
# Node ID 5fc3097708402d6ef066ab84eb9de339a259ab1a
# Parent  56ddf617d6e80338713d182119fdbed66f3f9685
add xsymbol syntax for u type constructor

diff -r 56ddf617d6e8 -r 5fc309770840 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Nov 30 00:53:30 2005 +0100
+++ b/src/HOLCF/Up.thy	Wed Nov 30 00:55:24 2005 +0100
@@ -17,6 +17,9 @@
 
 datatype 'a u = Ibottom | Iup 'a
 
+syntax (xsymbols)
+  "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
+
 consts
   Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
 
@@ -24,7 +27,7 @@
   "Ifup f Ibottom = \<bottom>"
   "Ifup f (Iup x) = f\<cdot>x"
 
-subsection {* Ordering on type @{typ "'a u"} *}
+subsection {* Ordering on lifted cpo *}
 
 instance u :: (sq_ord) sq_ord ..
 
@@ -42,7 +45,7 @@
 lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
 by (simp add: less_up_def)
 
-subsection {* Type @{typ "'a u"} is a partial order *}
+subsection {* Lifted cpo is a partial order *}
 
 lemma refl_less_up: "(x::'a u) \<sqsubseteq> x"
 by (simp add: less_up_def split: u.split)
@@ -61,7 +64,7 @@
 by intro_classes
   (assumption | rule refl_less_up antisym_less_up trans_less_up)+
 
-subsection {* Type @{typ "'a u"} is a cpo *}
+subsection {* Lifted cpo is a cpo *}
 
 lemma is_lub_Iup:
   "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
@@ -147,7 +150,7 @@
 instance u :: (cpo) cpo
 by intro_classes (rule cpo_up)
 
-subsection {* Type @{typ "'a u"} is pointed *}
+subsection {* Lifted cpo is pointed *}
 
 lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
 apply (rule_tac x = "Ibottom" in exI)