diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Sun May 06 21:49:44 2007 +0200
+++ b/src/HOL/FixedPoint.thy	Sun May 06 21:50:17 2007 +0200
@@ -14,18 +14,19 @@
 subsection {* Complete lattices *}
 
 class complete_lattice = lattice +
-  fixes Inf :: "'a set \<Rightarrow> 'a"
-  assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
-  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
+  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90)
+  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
+  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
 
 definition
-  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where
+  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a"
+where
   "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
 
-theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A"
+theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x \<le> Sup A"
   by (auto simp: Sup_def intro: Inf_greatest)
 
-theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
+theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
   by (auto simp: Sup_def intro: Inf_lower)
 
 definition
@@ -198,7 +199,7 @@
   apply (iprover elim: le_funE)
   done
 
-lemmas [code nofunc] = Inf_fun_def
+lemmas [code func del] = Inf_fun_def
 
 theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   apply (rule order_antisym)
@@ -221,7 +222,7 @@
   Inf_set_def: "Inf S \<equiv> \<Inter>S"
   by intro_classes (auto simp add: Inf_set_def)
 
-lemmas [code nofunc] = Inf_set_def
+lemmas [code func del] = Inf_set_def
 
 theorem Sup_set_eq: "Sup S = \<Union>S"
   apply (rule subset_antisym)