# HG changeset patch
# User haftmann
# Date 1179567202 -7200
# Node ID 1d29bc31b0cb6c98f67ebc01df5b80f0d62ba6b4
# Parent  00c0e4c42396e325d5b9af20724d59cc1a833591
no special treatment in naming of locale predicates stemming form classes

diff -r 00c0e4c42396 -r 1d29bc31b0cb src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat May 19 11:33:21 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Sat May 19 11:33:22 2007 +0200
@@ -2432,53 +2432,53 @@
 
 lemma ACIf_min: "ACIf min"
   by (rule lower_semilattice.ACIf_inf,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
 lemma ACf_min: "ACf min"
   by (rule lower_semilattice.ACf_inf,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
 lemma ACIfSL_min: "ACIfSL (op \<^loc>\<le>) (op \<^loc><) min"
   by (rule lower_semilattice.ACIfSL_inf,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
 lemma ACIfSLlin_min: "ACIfSLlin (op \<^loc>\<le>) (op \<^loc><) min"
   by (rule ACIfSLlin.intro,
     rule lower_semilattice.ACIfSL_inf,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
     (unfold_locales, simp add: min_def)
 
 lemma ACIf_max: "ACIf max"
   by (rule upper_semilattice.ACIf_sup,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
 lemma ACf_max: "ACf max"
   by (rule upper_semilattice.ACf_sup,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
 lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
   by (rule upper_semilattice.ACIfSL_sup,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
 lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
   by (rule ACIfSLlin.intro,
     rule upper_semilattice.ACIfSL_sup,
-    rule lattice_pred.axioms,
-    rule distrib_lattice_pred.axioms,
+    rule lattice.axioms,
+    rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
     (unfold_locales, simp add: max_def)
 
@@ -2601,7 +2601,7 @@
 proof
   fix A :: "'a set"
   show "Linorder.Min (op \<le>) A = Min A"
-  by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_pred_axioms]
+  by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_axioms]
     linorder_class_min)
 qed
 
@@ -2610,19 +2610,19 @@
 proof
   fix A :: "'a set"
   show "Linorder.Max (op \<le>) A = Max A"
-  by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_pred_axioms]
+  by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms]
     linorder_class_max)
 qed
 
 interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
   Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"]
   by (rule Linorder_ab_semigroup_add.intro,
-    rule Linorder.intro, rule linorder_pred_axioms, rule pordered_ab_semigroup_add_pred_axioms)
+    rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms)
 hide const Min Max
 
 interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
   Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
-  by (rule Linorder.intro, rule linorder_pred_axioms)
+  by (rule Linorder.intro, rule linorder_axioms)
 declare Min_singleton [simp]
 declare Max_singleton [simp]
 declare Min_insert [simp]
@@ -2640,8 +2640,11 @@
 
 subsection {* Class @{text finite} *}
 
+setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
 class finite (attach UNIV) = type +
   assumes finite: "finite UNIV"
+setup {* Sign.parent_path *}
+hide const finite
 
 lemma finite_set: "finite (A::'a::finite set)"
   by (rule finite_subset [OF subset_UNIV finite])
diff -r 00c0e4c42396 -r 1d29bc31b0cb src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat May 19 11:33:21 2007 +0200
+++ b/src/HOL/Lattices.thy	Sat May 19 11:33:22 2007 +0200
@@ -282,7 +282,7 @@
   special case of @{const inf}/@{const sup} *}
 
 lemma (in linorder) distrib_lattice_min_max:
-  "distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max"
+  "distrib_lattice (op \<^loc>\<le>) (op \<^loc><) min max"
 proof unfold_locales
   have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
     by (auto simp add: less_le antisym)
diff -r 00c0e4c42396 -r 1d29bc31b0cb src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat May 19 11:33:21 2007 +0200
+++ b/src/HOL/Orderings.thy	Sat May 19 11:33:22 2007 +0200
@@ -199,7 +199,7 @@
 text {* Reverse order *}
 
 lemma order_reverse:
-  "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+  "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
   by unfold_locales
     (simp add: less_le, auto intro: antisym order_trans)
 
@@ -266,7 +266,7 @@
 text {* Reverse order *}
 
 lemma linorder_reverse:
-  "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+  "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
   by unfold_locales
     (simp add: less_le, auto intro: antisym order_trans simp add: linear)
 
diff -r 00c0e4c42396 -r 1d29bc31b0cb src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sat May 19 11:33:21 2007 +0200
+++ b/src/Pure/Tools/class_package.ML	Sat May 19 11:33:22 2007 +0200
@@ -561,7 +561,7 @@
       #> snd
   in
     thy
-    |> add_locale (SOME (bname ^ "_pred")) bname supexpr ((*elems_constrains @*) elems)
+    |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
     |-> (fn name_locale => ProofContext.theory_result (
       `(fn thy => extract_params thy name_locale)
       #-> (fn (param_names, params) =>