proper class syntax for sublocale class < expr
authorhaftmann
Thu Sep 03 15:39:02 2009 +0200 (2009-09-03)
changeset 32512d14762642cdd
parent 32490 6a48db3e627c
child 32513 94f61caa546e
proper class syntax for sublocale class < expr
src/HOL/Lattices.thy
src/Pure/Isar/expression.ML
     1.1 --- a/src/HOL/Lattices.thy	Wed Sep 02 14:11:45 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Thu Sep 03 15:39:02 2009 +0200
     1.3 @@ -413,12 +413,11 @@
     1.4  subsection {* @{const min}/@{const max} on linear orders as
     1.5    special case of @{const inf}/@{const sup} *}
     1.6  
     1.7 -sublocale linorder < min_max!: distrib_lattice less_eq less "Orderings.ord.min less_eq" "Orderings.ord.max less_eq"
     1.8 +sublocale linorder < min_max!: distrib_lattice less_eq less min max
     1.9  proof
    1.10    fix x y z
    1.11 -  show "Orderings.ord.max less_eq x (Orderings.ord.min less_eq y z) =
    1.12 -    Orderings.ord.min less_eq (Orderings.ord.max less_eq x y) (Orderings.ord.max less_eq x z)"
    1.13 -  unfolding min_def max_def by auto
    1.14 +  show "max x (min y z) = min (max x y) (max x z)"
    1.15 +    by (auto simp add: min_def max_def)
    1.16  qed (auto simp add: min_def max_def not_le less_imp_le)
    1.17  
    1.18  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.19 @@ -514,9 +513,6 @@
    1.20    inf_compl_bot sup_compl_top diff_eq)
    1.21  
    1.22  
    1.23 -text {* redundant bindings *}
    1.24 -
    1.25 -
    1.26  no_notation
    1.27    less_eq  (infix "\<sqsubseteq>" 50) and
    1.28    less (infix "\<sqsubset>" 50) and
     2.1 --- a/src/Pure/Isar/expression.ML	Wed Sep 02 14:11:45 2009 +0200
     2.2 +++ b/src/Pure/Isar/expression.ML	Thu Sep 03 15:39:02 2009 +0200
     2.3 @@ -839,7 +839,7 @@
     2.4  fun gen_sublocale prep_expr intern raw_target expression thy =
     2.5    let
     2.6      val target = intern thy raw_target;
     2.7 -    val target_ctxt = Locale.init target thy;
     2.8 +    val target_ctxt = TheoryTarget.init (SOME target) thy;
     2.9      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    2.10      fun after_qed witss = ProofContext.theory
    2.11        (fold (fn ((dep, morph), wits) => Locale.add_dependency