# HG changeset patch
# User wenzelm
# Date 1394052690 -3600
# Node ID 3ef14caf5637843ba00f4d9ece75694166fc3860
# Parent  56165322c98b29289f3210d508d676d351d356fe
more symbols;

diff -r 56165322c98b -r 3ef14caf5637 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 20:07:43 2014 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 21:51:30 2014 +0100
@@ -54,8 +54,8 @@
 locale abelian_group_hom = G: abelian_group G + H: abelian_group H
     for G (structure) and H (structure) +
   fixes h
-  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
-                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
+  assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
+                                  \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
 
 lemmas a_r_coset_defs =
   a_r_coset_def r_coset_def
@@ -129,12 +129,12 @@
     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
 
 lemma (in abelian_group) a_coset_join1:
-     "[| H +> x = H;  x \<in> carrier G;  subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \<in> H"
+     "[| H +> x = H;  x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H"
 by (rule group.coset_join1 [OF a_group,
     folded a_r_coset_def, simplified monoid_record_simps])
 
 lemma (in abelian_group) a_solve_equation:
-    "\<lbrakk>subgroup H (|carrier = carrier G, mult = add G, one = zero G|); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
+    "\<lbrakk>subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
 by (rule group.solve_equation [OF a_group,
     folded a_r_coset_def, simplified monoid_record_simps])
 
@@ -535,8 +535,8 @@
 lemma abelian_group_homI:
   assumes "abelian_group G"
   assumes "abelian_group H"
-  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
-                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
+  assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
+                                  \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
   shows "abelian_group_hom G H h"
 proof -
   interpret G: abelian_group G by fact
@@ -636,7 +636,7 @@
 theorem (in abelian_group_hom) A_FactGroup_iso:
   "h ` carrier G = carrier H
    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
-          (| carrier = carrier H, mult = add H, one = zero H |)"
+          \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
 by (rule group_hom.FactGroup_iso[OF a_group_hom,
     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
 
diff -r 56165322c98b -r 3ef14caf5637 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Mar 05 20:07:43 2014 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Mar 05 21:51:30 2014 +0100
@@ -721,7 +721,7 @@
 text_raw {* \label{sec:subgroup-lattice} *}
 
 theorem (in group) subgroups_partial_order:
-  "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
+  "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
   by default simp_all
 
 lemma (in group) subgroup_self:
@@ -729,7 +729,7 @@
   by (rule subgroupI) auto
 
 lemma (in group) subgroup_imp_group:
-  "subgroup H G ==> group (G(| carrier := H |))"
+  "subgroup H G ==> group (G\<lparr>carrier := H\<rparr>)"
   by (erule subgroup.subgroup_is_group) (rule group_axioms)
 
 lemma (in group) is_monoid [intro, simp]:
@@ -737,7 +737,7 @@
   by (auto intro: monoid.intro m_assoc) 
 
 lemma (in group) subgroup_inv_equality:
-  "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
+  "[| subgroup H G; x \<in> H |] ==> m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
 apply (rule_tac inv_equality [THEN sym])
   apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
  apply (rule subsetD [OF subgroup.subset], assumption+)
@@ -766,7 +766,7 @@
 qed
 
 theorem (in group) subgroups_complete_lattice:
-  "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
+  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
     (is "complete_lattice ?L")
 proof (rule partial_order.complete_lattice_criterion1)
   show "partial_order ?L" by (rule subgroups_partial_order)
@@ -784,7 +784,7 @@
     fix H
     assume H: "H \<in> A"
     with L have subgroupH: "subgroup H G" by auto
-    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
+    from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H")
       by (rule subgroup_imp_group)
     from groupH have monoidH: "monoid ?H"
       by (rule group.is_monoid)
diff -r 56165322c98b -r 3ef14caf5637 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Wed Mar 05 20:07:43 2014 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Wed Mar 05 21:51:30 2014 +0100
@@ -23,7 +23,7 @@
 
 abbreviation
   int_ring :: "int ring" ("\<Z>") where
-  "int_ring == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+  "int_ring == \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
 
 lemma int_Zcarr [intro!, simp]:
   "k \<in> carrier \<Z>"
@@ -183,27 +183,27 @@
   by simp_all
 
 interpretation int (* FIXME [unfolded UNIV] *) :
-  partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
-  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
-    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
-    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
+  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
+  where "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
+    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
+    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
 proof -
-  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
+  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
     by default simp_all
-  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
+  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
     by simp
-  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
+  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
     by simp
-  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
+  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
     by (simp add: lless_def) auto
 qed
 
 interpretation int (* FIXME [unfolded UNIV] *) :
-  lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
-  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
-    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
+  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
+  where "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
+    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
 proof -
-  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
+  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
   show "lattice ?Z"
     apply unfold_locales
     apply (simp add: least_def Upper_def)
@@ -225,7 +225,7 @@
 qed
 
 interpretation int (* [unfolded UNIV] *) :
-  total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
+  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
   by default clarsimp
 
 
diff -r 56165322c98b -r 3ef14caf5637 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Mar 05 20:07:43 2014 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Wed Mar 05 21:51:30 2014 +0100
@@ -1278,7 +1278,7 @@
 subsubsection {* The Powerset of a Set is a Complete Lattice *}
 
 theorem powerset_is_complete_lattice:
-  "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
+  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)
   show "partial_order ?L"
diff -r 56165322c98b -r 3ef14caf5637 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Mar 05 20:07:43 2014 +0100
+++ b/src/HOL/Algebra/Ring.thy	Wed Mar 05 21:51:30 2014 +0100
@@ -19,7 +19,7 @@
 
 definition
   a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
-  where "a_inv R = m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+  where "a_inv R = m_inv \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
 
 definition
   a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
@@ -28,11 +28,11 @@
 locale abelian_monoid =
   fixes G (structure)
   assumes a_comm_monoid:
-     "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"
+     "comm_monoid \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 definition
   finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
-  "finsum G = finprod (| carrier = carrier G, mult = add G, one = zero G |)"
+  "finsum G = finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 syntax
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
@@ -50,7 +50,7 @@
 
 locale abelian_group = abelian_monoid +
   assumes a_comm_group:
-     "comm_group (| carrier = carrier G, mult = add G, one = zero G |)"
+     "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 
 subsection {* Basic Properties *}
@@ -87,11 +87,11 @@
     intro: assms)
 
 lemma (in abelian_monoid) a_monoid:
-  "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
+  "monoid \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 by (rule comm_monoid.axioms, rule a_comm_monoid) 
 
 lemma (in abelian_group) a_group:
-  "group (| carrier = carrier G, mult = add G, one = zero G |)"
+  "group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   by (simp add: group_def a_monoid)
     (simp add: comm_group.axioms group.axioms a_comm_group)
 
@@ -100,10 +100,10 @@
 text {* Transfer facts from multiplicative structures via interpretation. *}
 
 sublocale abelian_monoid <
-  add!: monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
-  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
-    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
-    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
+  add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
+    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
   by (rule a_monoid) auto
 
 context abelian_monoid begin
@@ -118,11 +118,11 @@
 end
 
 sublocale abelian_monoid <
-  add!: comm_monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
-  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
-    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
-    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
-    and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
+  add!: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
+    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
+    and "finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = finsum G"
   by (rule a_comm_monoid) (auto simp: finsum_def)
 
 context abelian_monoid begin
@@ -173,14 +173,15 @@
 end
 
 sublocale abelian_group <
-  add!: group "(| carrier = carrier G, mult = add G, one = zero G |)"
-  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
-    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
-    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
-    and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
+  add!: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
+    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
+    and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
   by (rule a_group) (auto simp: m_inv_def a_inv_def)
 
-context abelian_group begin
+context abelian_group
+begin
 
 lemmas a_inv_closed = add.inv_closed
 
@@ -200,12 +201,12 @@
 end
 
 sublocale abelian_group <
-  add!: comm_group "(| carrier = carrier G, mult = add G, one = zero G |)"
-  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
-    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
-    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
-    and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
-    and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
+  add!: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
+    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
+    and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
+    and "finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = finsum G"
   by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def)
 
 lemmas (in abelian_group) minus_add = add.inv_mult
diff -r 56165322c98b -r 3ef14caf5637 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 20:07:43 2014 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 21:51:30 2014 +0100
@@ -57,7 +57,7 @@
   where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
 
 definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
-  where "UP R = (|
+  where "UP R = \<lparr>
    carrier = up R,
    mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
    one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
@@ -65,7 +65,7 @@
    add = (%p:up R. %q:up R. %i. p i \<oplus>\<^bsub>R\<^esub> q i),
    smult = (%a:carrier R. %p:up R. %i. a \<otimes>\<^bsub>R\<^esub> p i),
    monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
-   coeff = (%p:up R. %n. p n) |)"
+   coeff = (%p:up R. %n. p n)\<rparr>"
 
 text {*
   Properties of the set of polynomials @{term up}.
@@ -1814,7 +1814,7 @@
 
 definition
   INTEG :: "int ring"
-  where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+  where "INTEG = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
 
 lemma INTEG_cring: "cring INTEG"
   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI