1.1 --- a/etc/isar-keywords-ZF.el	Fri Dec 12 17:00:42 2008 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Fri Dec 12 20:03:30 2008 +0100
     1.3 @@ -40,6 +40,9 @@
     1.4      "chapter"
     1.5      "class"
     1.6      "class_deps"
     1.7 +    "class_interpret"
     1.8 +    "class_interpretation"
     1.9 +    "class_locale"
    1.10      "classes"
    1.11      "classrel"
    1.12      "codatatype"
    1.13 @@ -349,6 +352,7 @@
    1.14      "axiomatization"
    1.15      "axioms"
    1.16      "class"
    1.17 +    "class_locale"
    1.18      "classes"
    1.19      "classrel"
    1.20      "codatatype"
    1.21 @@ -411,7 +415,8 @@
    1.22    '("inductive_cases"))
    1.23  
    1.24  (defconst isar-keywords-theory-goal
    1.25 -  '("corollary"
    1.26 +  '("class_interpretation"
    1.27 +    "corollary"
    1.28      "instance"
    1.29      "interpretation"
    1.30      "lemma"
    1.31 @@ -438,7 +443,8 @@
    1.32      "subsubsect"))
    1.33  
    1.34  (defconst isar-keywords-proof-goal
    1.35 -  '("have"
    1.36 +  '("class_interpret"
    1.37 +    "have"
    1.38      "hence"
    1.39      "interpret"
    1.40      "invoke"))

     2.1 --- a/src/HOL/Library/Dense_Linear_Order.thy	Fri Dec 12 17:00:42 2008 +0100
     2.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy	Fri Dec 12 20:03:30 2008 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*
     2.5 -    ID:         $Id$
     2.6      Author:     Amine Chaieb, TU Muenchen
     2.7  *)
     2.8  
     2.9 @@ -304,7 +303,7 @@
    2.10  
    2.11  text {* Linear order without upper bounds *}
    2.12  
    2.13 -locale linorder_stupid_syntax = linorder
    2.14 +class_locale linorder_stupid_syntax = linorder
    2.15  begin
    2.16  notation
    2.17    less_eq  ("op \<sqsubseteq>") and
    2.18 @@ -314,7 +313,7 @@
    2.19  
    2.20  end
    2.21  
    2.22 -locale linorder_no_ub = linorder_stupid_syntax +
    2.23 +class_locale linorder_no_ub = linorder_stupid_syntax +
    2.24    assumes gt_ex: "\<exists>y. less x y"
    2.25  begin
    2.26  lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
    2.27 @@ -363,7 +362,7 @@
    2.28  
    2.29  text {* Linear order without upper bounds *}
    2.30  
    2.31 -locale linorder_no_lb = linorder_stupid_syntax +
    2.32 +class_locale linorder_no_lb = linorder_stupid_syntax +
    2.33    assumes lt_ex: "\<exists>y. less y x"
    2.34  begin
    2.35  lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
    2.36 @@ -410,12 +409,12 @@
    2.37  end
    2.38  
    2.39  
    2.40 -locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
    2.41 +class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
    2.42    fixes between
    2.43    assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
    2.44       and  between_same: "between x x = x"
    2.45  
    2.46 -interpretation  constr_dense_linear_order < dense_linear_order 
    2.47 +class_interpretation  constr_dense_linear_order < dense_linear_order 
    2.48    apply unfold_locales
    2.49    using gt_ex lt_ex between_less
    2.50      by (auto, rule_tac x="between x y" in exI, simp)
    2.51 @@ -638,7 +637,7 @@
    2.52    using eq_diff_eq[where a= x and b=t and c=0] by simp
    2.53  
    2.54  
    2.55 -interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
    2.56 +class_interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
    2.57   ["op <=" "op <"
    2.58     "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
    2.59  proof (unfold_locales, dlo, dlo, auto)

     3.1 --- a/src/HOL/Real/RealVector.thy	Fri Dec 12 17:00:42 2008 +0100
     3.2 +++ b/src/HOL/Real/RealVector.thy	Fri Dec 12 20:03:30 2008 +0100
     3.3 @@ -60,7 +60,7 @@
     3.4    and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
     3.5    and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
     3.6  proof -
     3.7 -  interpret s: additive ["\<lambda>a. scale a x"]
     3.8 +  interpret s: additive "\<lambda>a. scale a x"
     3.9      proof qed (rule scale_left_distrib)
    3.10    show "scale 0 x = 0" by (rule s.zero)
    3.11    show "scale (- a) x = - (scale a x)" by (rule s.minus)
    3.12 @@ -71,7 +71,7 @@
    3.13    and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
    3.14    and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
    3.15  proof -
    3.16 -  interpret s: additive ["\<lambda>x. scale a x"]
    3.17 +  interpret s: additive "\<lambda>x. scale a x"
    3.18      proof qed (rule scale_right_distrib)
    3.19    show "scale a 0 = 0" by (rule s.zero)
    3.20    show "scale a (- x) = - (scale a x)" by (rule s.minus)
    3.21 @@ -152,7 +152,7 @@
    3.22    and scaleR_one [simp]: "scaleR 1 x = x"
    3.23  
    3.24  interpretation real_vector:
    3.25 -  vector_space ["scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"]
    3.26 +  vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
    3.27  apply unfold_locales
    3.28  apply (rule scaleR_right_distrib)
    3.29  apply (rule scaleR_left_distrib)
    3.30 @@ -195,10 +195,10 @@
    3.31  apply (rule mult_left_commute)
    3.32  done
    3.33  
    3.34 -interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
    3.35 +interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
    3.36  proof qed (rule scaleR_left_distrib)
    3.37  
    3.38 -interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
    3.39 +interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
    3.40  proof qed (rule scaleR_right_distrib)
    3.41  
    3.42  lemma nonzero_inverse_scaleR_distrib:
    3.43 @@ -797,7 +797,7 @@
    3.44  end
    3.45  
    3.46  interpretation mult:
    3.47 -  bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
    3.48 +  bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
    3.49  apply (rule bounded_bilinear.intro)
    3.50  apply (rule left_distrib)
    3.51  apply (rule right_distrib)
    3.52 @@ -808,18 +808,18 @@
    3.53  done
    3.54  
    3.55  interpretation mult_left:
    3.56 -  bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
    3.57 +  bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
    3.58  by (rule mult.bounded_linear_left)
    3.59  
    3.60  interpretation mult_right:
    3.61 -  bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
    3.62 +  bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
    3.63  by (rule mult.bounded_linear_right)
    3.64  
    3.65  interpretation divide:
    3.66 -  bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
    3.67 +  bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
    3.68  unfolding divide_inverse by (rule mult.bounded_linear_left)
    3.69  
    3.70 -interpretation scaleR: bounded_bilinear ["scaleR"]
    3.71 +interpretation scaleR: bounded_bilinear "scaleR"
    3.72  apply (rule bounded_bilinear.intro)
    3.73  apply (rule scaleR_left_distrib)
    3.74  apply (rule scaleR_right_distrib)
    3.75 @@ -829,13 +829,13 @@
    3.76  apply (simp add: norm_scaleR)
    3.77  done
    3.78  
    3.79 -interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"]
    3.80 +interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
    3.81  by (rule scaleR.bounded_linear_left)
    3.82  
    3.83 -interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"]
    3.84 +interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
    3.85  by (rule scaleR.bounded_linear_right)
    3.86  
    3.87 -interpretation of_real: bounded_linear ["\<lambda>r. of_real r"]
    3.88 +interpretation of_real: bounded_linear "\<lambda>r. of_real r"
    3.89  unfolding of_real_def by (rule scaleR.bounded_linear_left)
    3.90  
    3.91  end