# HG changeset patch
# User ballarin
# Date 1229108610 -3600
# Node ID 6f6262027054ce7796cf02d9d991f3c39936af56
# Parent  40b3630b0deb49f461de289917204c05f8d32967
Porting to new locales.

diff -r 40b3630b0deb -r 6f6262027054 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Fri Dec 12 17:00:42 2008 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Dec 12 20:03:30 2008 +0100
@@ -40,6 +40,9 @@
     "chapter"
     "class"
     "class_deps"
+    "class_interpret"
+    "class_interpretation"
+    "class_locale"
     "classes"
     "classrel"
     "codatatype"
@@ -349,6 +352,7 @@
     "axiomatization"
     "axioms"
     "class"
+    "class_locale"
     "classes"
     "classrel"
     "codatatype"
@@ -411,7 +415,8 @@
   '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal
-  '("corollary"
+  '("class_interpretation"
+    "corollary"
     "instance"
     "interpretation"
     "lemma"
@@ -438,7 +443,8 @@
     "subsubsect"))
 
 (defconst isar-keywords-proof-goal
-  '("have"
+  '("class_interpret"
+    "have"
     "hence"
     "interpret"
     "invoke"))
diff -r 40b3630b0deb -r 6f6262027054 src/HOL/Library/Dense_Linear_Order.thy
--- a/src/HOL/Library/Dense_Linear_Order.thy	Fri Dec 12 17:00:42 2008 +0100
+++ b/src/HOL/Library/Dense_Linear_Order.thy	Fri Dec 12 20:03:30 2008 +0100
@@ -1,5 +1,4 @@
 (*
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -304,7 +303,7 @@
 
 text {* Linear order without upper bounds *}
 
-locale linorder_stupid_syntax = linorder
+class_locale linorder_stupid_syntax = linorder
 begin
 notation
   less_eq  ("op \<sqsubseteq>") and
@@ -314,7 +313,7 @@
 
 end
 
-locale linorder_no_ub = linorder_stupid_syntax +
+class_locale linorder_no_ub = linorder_stupid_syntax +
   assumes gt_ex: "\<exists>y. less x y"
 begin
 lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
@@ -363,7 +362,7 @@
 
 text {* Linear order without upper bounds *}
 
-locale linorder_no_lb = linorder_stupid_syntax +
+class_locale linorder_no_lb = linorder_stupid_syntax +
   assumes lt_ex: "\<exists>y. less y x"
 begin
 lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
@@ -410,12 +409,12 @@
 end
 
 
-locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
+class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   fixes between
   assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
      and  between_same: "between x x = x"
 
-interpretation  constr_dense_linear_order < dense_linear_order 
+class_interpretation  constr_dense_linear_order < dense_linear_order 
   apply unfold_locales
   using gt_ex lt_ex between_less
     by (auto, rule_tac x="between x y" in exI, simp)
@@ -638,7 +637,7 @@
   using eq_diff_eq[where a= x and b=t and c=0] by simp
 
 
-interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
+class_interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
  ["op <=" "op <"
    "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
 proof (unfold_locales, dlo, dlo, auto)
diff -r 40b3630b0deb -r 6f6262027054 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri Dec 12 17:00:42 2008 +0100
+++ b/src/HOL/Real/RealVector.thy	Fri Dec 12 20:03:30 2008 +0100
@@ -60,7 +60,7 @@
   and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
   and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
 proof -
-  interpret s: additive ["\<lambda>a. scale a x"]
+  interpret s: additive "\<lambda>a. scale a x"
     proof qed (rule scale_left_distrib)
   show "scale 0 x = 0" by (rule s.zero)
   show "scale (- a) x = - (scale a x)" by (rule s.minus)
@@ -71,7 +71,7 @@
   and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
   and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
 proof -
-  interpret s: additive ["\<lambda>x. scale a x"]
+  interpret s: additive "\<lambda>x. scale a x"
     proof qed (rule scale_right_distrib)
   show "scale a 0 = 0" by (rule s.zero)
   show "scale a (- x) = - (scale a x)" by (rule s.minus)
@@ -152,7 +152,7 @@
   and scaleR_one [simp]: "scaleR 1 x = x"
 
 interpretation real_vector:
-  vector_space ["scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"]
+  vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
 apply unfold_locales
 apply (rule scaleR_right_distrib)
 apply (rule scaleR_left_distrib)
@@ -195,10 +195,10 @@
 apply (rule mult_left_commute)
 done
 
-interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
+interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
 proof qed (rule scaleR_left_distrib)
 
-interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
+interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
 proof qed (rule scaleR_right_distrib)
 
 lemma nonzero_inverse_scaleR_distrib:
@@ -797,7 +797,7 @@
 end
 
 interpretation mult:
-  bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
+  bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
 apply (rule bounded_bilinear.intro)
 apply (rule left_distrib)
 apply (rule right_distrib)
@@ -808,18 +808,18 @@
 done
 
 interpretation mult_left:
-  bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
+  bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
 by (rule mult.bounded_linear_left)
 
 interpretation mult_right:
-  bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
+  bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
 by (rule mult.bounded_linear_right)
 
 interpretation divide:
-  bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
+  bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
 unfolding divide_inverse by (rule mult.bounded_linear_left)
 
-interpretation scaleR: bounded_bilinear ["scaleR"]
+interpretation scaleR: bounded_bilinear "scaleR"
 apply (rule bounded_bilinear.intro)
 apply (rule scaleR_left_distrib)
 apply (rule scaleR_right_distrib)
@@ -829,13 +829,13 @@
 apply (simp add: norm_scaleR)
 done
 
-interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"]
+interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
 by (rule scaleR.bounded_linear_left)
 
-interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"]
+interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
 by (rule scaleR.bounded_linear_right)
 
-interpretation of_real: bounded_linear ["\<lambda>r. of_real r"]
+interpretation of_real: bounded_linear "\<lambda>r. of_real r"
 unfolding of_real_def by (rule scaleR.bounded_linear_left)
 
 end