# HG changeset patch
# User wenzelm
# Date 1144601473 -7200
# Node ID b808efaa5828f6c33313efcc3a76377b9e8f5064
# Parent  c8cf1544b5a7b86703e3f1302316fb1f1c2e3057
tuned syntax/abbreviations;

diff -r c8cf1544b5a7 -r b808efaa5828 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/FOL/IFOL.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -50,12 +50,12 @@
   "x ~= y == ~ (x = y)"
 
 abbreviation (xsymbols)
-  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
+  not_equal1  (infixl "\<noteq>" 50)
   "x \<noteq> y == ~ (x = y)"
 
 abbreviation (HTML output)
-  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
-  "not_equal == xsymbols.not_equal"
+  not_equal2  (infixl "\<noteq>" 50)
+  "not_equal2 == not_equal"
 
 syntax (xsymbols)
   Not           :: "o => o"                     ("\<not> _" [40] 40)
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Algebra/Coset.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -27,12 +27,9 @@
 locale normal = subgroup + group +
   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
 
-
-syntax
-  "@normal" :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
-
-translations
-  "H \<lhd> G" == "normal H G"
+abbreviation
+  normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
+  "H \<lhd> G \<equiv> normal H G"
 
 
 subsection {*Basic Properties of Cosets*}
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -14,8 +14,9 @@
 
 types hypreal = "real star"
 
-syntax hypreal_of_real :: "real => real star"
-translations "hypreal_of_real" => "star_of :: real => real star"
+abbreviation
+  hypreal_of_real :: "real => real star"
+  "hypreal_of_real == star_of"
 
 constdefs
 
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -13,8 +13,9 @@
 
 types hypnat = "nat star"
 
-syntax hypnat_of_nat :: "nat => nat star"
-translations "hypnat_of_nat" => "star_of :: nat => nat star"
+abbreviation
+  hypnat_of_nat :: "nat => nat star"
+  "hypnat_of_nat == star_of"
 
 subsection{*Properties Transferred from Naturals*}
 
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -18,7 +18,19 @@
 
 defs (overloaded)
   nat_number_of_def:
-     "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
+  "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
+
+abbreviation (xsymbols)
+  square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
+  "x\<twosuperior> == x^2"
+
+abbreviation (latex output)
+  square1  ("(_\<twosuperior>)" [1000] 999)
+  "square1 x == x^2"
+
+abbreviation (HTML output)
+  square2  ("(_\<twosuperior>)" [1000] 999)
+  "square2 x == x^2"
 
 
 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Integ/Numeral.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -11,11 +11,6 @@
 uses "../Tools/numeral_syntax.ML"
 begin
 
-text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
-   Only qualified access Numeral.Pls and Numeral.Min is allowed.
-   The datatype constructors bit.B0 and bit.B1 are similarly hidden.
-   We do not hide Bit because we need the BIT infix syntax.*}
-
 text{*This formalization defines binary arithmetic in terms of the integers
 rather than using a datatype. This avoids multiple representations (leading
 zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
@@ -58,26 +53,12 @@
 
 syntax
   "_Numeral" :: "num_const => 'a"    ("_")
-  Numeral0 :: 'a
-  Numeral1 :: 'a
-
-translations
-  "Numeral0" == "number_of Numeral.Pls"
-  "Numeral1" == "number_of (Numeral.Pls BIT bit.B1)"
-
 
 setup NumeralSyntax.setup
 
-syntax (xsymbols)
-  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
-syntax (HTML output)
-  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
-syntax (output)
-  "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
-translations
-  "x\<twosuperior>" == "x^2"
-  "x\<twosuperior>" <= "x^(2::nat)"
-
+abbreviation
+  "Numeral0 == number_of Pls"
+  "Numeral1 == number_of (Pls BIT B1)"
 
 lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
   -- {* Unfold all @{text let}s involving constants *}
@@ -112,90 +93,90 @@
        Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
 
 text{*Removal of leading zeroes*}
-lemma Pls_0_eq [simp]: "Numeral.Pls BIT bit.B0 = Numeral.Pls"
+lemma Pls_0_eq [simp]: "Pls BIT B0 = Pls"
 by (simp add: Bin_simps)
 
-lemma Min_1_eq [simp]: "Numeral.Min BIT bit.B1 = Numeral.Min"
+lemma Min_1_eq [simp]: "Min BIT B1 = Min"
 by (simp add: Bin_simps)
 
 subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
 
-lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1"
+lemma bin_succ_Pls [simp]: "bin_succ Pls = Pls BIT B1"
 by (simp add: Bin_simps) 
 
-lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
+lemma bin_succ_Min [simp]: "bin_succ Min = Pls"
 by (simp add: Bin_simps) 
 
-lemma bin_succ_1 [simp]: "bin_succ(w BIT bit.B1) = (bin_succ w) BIT bit.B0"
+lemma bin_succ_1 [simp]: "bin_succ(w BIT B1) = (bin_succ w) BIT B0"
 by (simp add: Bin_simps add_ac) 
 
-lemma bin_succ_0 [simp]: "bin_succ(w BIT bit.B0) = w BIT bit.B1"
+lemma bin_succ_0 [simp]: "bin_succ(w BIT B0) = w BIT B1"
 by (simp add: Bin_simps add_ac) 
 
-lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
+lemma bin_pred_Pls [simp]: "bin_pred Pls = Min"
 by (simp add: Bin_simps) 
 
-lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT bit.B0"
+lemma bin_pred_Min [simp]: "bin_pred Min = Min BIT B0"
 by (simp add: Bin_simps diff_minus) 
 
-lemma bin_pred_1 [simp]: "bin_pred(w BIT bit.B1) = w BIT bit.B0"
+lemma bin_pred_1 [simp]: "bin_pred(w BIT B1) = w BIT B0"
 by (simp add: Bin_simps) 
 
-lemma bin_pred_0 [simp]: "bin_pred(w BIT bit.B0) = (bin_pred w) BIT bit.B1"
+lemma bin_pred_0 [simp]: "bin_pred(w BIT B0) = (bin_pred w) BIT B1"
 by (simp add: Bin_simps diff_minus add_ac) 
 
-lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
+lemma bin_minus_Pls [simp]: "bin_minus Pls = Pls"
 by (simp add: Bin_simps) 
 
-lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT bit.B1"
+lemma bin_minus_Min [simp]: "bin_minus Min = Pls BIT B1"
 by (simp add: Bin_simps) 
 
 lemma bin_minus_1 [simp]:
-     "bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1"
+     "bin_minus (w BIT B1) = bin_pred (bin_minus w) BIT B1"
 by (simp add: Bin_simps add_ac diff_minus) 
 
- lemma bin_minus_0 [simp]: "bin_minus(w BIT bit.B0) = (bin_minus w) BIT bit.B0"
+ lemma bin_minus_0 [simp]: "bin_minus(w BIT B0) = (bin_minus w) BIT B0"
 by (simp add: Bin_simps) 
 
 
 subsection{*Binary Addition and Multiplication:
          @{term bin_add} and @{term bin_mult}*}
 
-lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
+lemma bin_add_Pls [simp]: "bin_add Pls w = w"
 by (simp add: Bin_simps) 
 
-lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
+lemma bin_add_Min [simp]: "bin_add Min w = bin_pred w"
 by (simp add: Bin_simps diff_minus add_ac) 
 
 lemma bin_add_BIT_11 [simp]:
-     "bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0"
+     "bin_add (v BIT B1) (w BIT B1) = bin_add v (bin_succ w) BIT B0"
 by (simp add: Bin_simps add_ac)
 
 lemma bin_add_BIT_10 [simp]:
-     "bin_add (v BIT bit.B1) (w BIT bit.B0) = (bin_add v w) BIT bit.B1"
+     "bin_add (v BIT B1) (w BIT B0) = (bin_add v w) BIT B1"
 by (simp add: Bin_simps add_ac)
 
 lemma bin_add_BIT_0 [simp]:
-     "bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y"
+     "bin_add (v BIT B0) (w BIT y) = bin_add v w BIT y"
 by (simp add: Bin_simps add_ac)
 
-lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
+lemma bin_add_Pls_right [simp]: "bin_add w Pls = w"
 by (simp add: Bin_simps) 
 
-lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
+lemma bin_add_Min_right [simp]: "bin_add w Min = bin_pred w"
 by (simp add: Bin_simps diff_minus) 
 
-lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
+lemma bin_mult_Pls [simp]: "bin_mult Pls w = Pls"
 by (simp add: Bin_simps) 
 
-lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
+lemma bin_mult_Min [simp]: "bin_mult Min w = bin_minus w"
 by (simp add: Bin_simps) 
 
 lemma bin_mult_1 [simp]:
-     "bin_mult (v BIT bit.B1) w = bin_add ((bin_mult v w) BIT bit.B0) w"
+     "bin_mult (v BIT B1) w = bin_add ((bin_mult v w) BIT B0) w"
 by (simp add: Bin_simps add_ac left_distrib)
 
-lemma bin_mult_0 [simp]: "bin_mult (v BIT bit.B0) w = (bin_mult v w) BIT bit.B0"
+lemma bin_mult_0 [simp]: "bin_mult (v BIT B0) w = (bin_mult v w) BIT B0"
 by (simp add: Bin_simps left_distrib)
 
 
@@ -228,7 +209,7 @@
 text{*The correctness of shifting.  But it doesn't seem to give a measurable
   speed-up.*}
 lemma double_number_of_BIT:
-     "(1+1) * number_of w = (number_of (w BIT bit.B0) ::'a::number_ring)"
+     "(1+1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
 by (simp add: number_of_eq Bin_simps left_distrib) 
 
 text{*Converting numerals 0 and 1 to their abstract versions*}
@@ -264,14 +245,14 @@
 by (simp add: diff_minus number_of_add number_of_minus)
 
 
-lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
+lemma number_of_Pls: "number_of Pls = (0::'a::number_ring)"
 by (simp add: number_of_eq Bin_simps) 
 
-lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
+lemma number_of_Min: "number_of Min = (- 1::'a::number_ring)"
 by (simp add: number_of_eq Bin_simps) 
 
 lemma number_of_BIT:
-     "number_of(w BIT x) = (case x of bit.B0 => 0 | bit.B1 => (1::'a::number_ring)) +
+     "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring)) +
 	                   (number_of w) + (number_of w)"
 by (simp add: number_of_eq Bin_simps split: bit.split) 
 
@@ -286,10 +267,10 @@
    iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
 by (simp add: iszero_def compare_rls number_of_add number_of_minus)
 
-lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
+lemma iszero_number_of_Pls: "iszero ((number_of Pls)::'a::number_ring)"
 by (simp add: iszero_def numeral_0_eq_0)
 
-lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
+lemma nonzero_number_of_Min: "~ iszero ((number_of Min)::'a::number_ring)"
 by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
 
 
@@ -353,17 +334,17 @@
 
 lemma iszero_number_of_BIT:
      "iszero (number_of (w BIT x)::'a) = 
-      (x=bit.B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
+      (x=B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
 by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
               Ints_odd_nonzero Ints_def split: bit.split)
 
 lemma iszero_number_of_0:
-     "iszero (number_of (w BIT bit.B0) :: 'a::{ordered_idom,number_ring}) = 
+     "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
       iszero (number_of w :: 'a)"
 by (simp only: iszero_number_of_BIT simp_thms)
 
 lemma iszero_number_of_1:
-     "~ iszero (number_of (w BIT bit.B1)::'a::{ordered_idom,number_ring})"
+     "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
 by (simp add: iszero_number_of_BIT) 
 
 
@@ -377,13 +358,13 @@
 done
 
 text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
-  @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
+  @{term Numeral0} IS @{term "number_of Pls"} *}
 lemma not_neg_number_of_Pls:
-     "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
+     "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
 by (simp add: neg_def numeral_0_eq_0)
 
 lemma neg_number_of_Min:
-     "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
+     "neg (number_of Min ::'a::{ordered_idom,number_ring})"
 by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
 
 lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
@@ -511,4 +492,7 @@
 apply (simp only: compare_rls)
 done
 
+
+hide (open) const Pls Min B0 B1
+
 end
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Integ/Parity.thy
--- a/src/HOL/Integ/Parity.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Integ/Parity.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -11,22 +11,20 @@
 
 axclass even_odd < type
 
-instance int :: even_odd ..
-instance nat :: even_odd ..
-
 consts
   even :: "'a::even_odd => bool"
 
-syntax 
-  odd :: "'a::even_odd => bool"
-
-translations 
-  "odd x" == "~even x" 
+instance int :: even_odd ..
+instance nat :: even_odd ..
 
 defs (overloaded)
   even_def: "even (x::int) == x mod 2 = 0"
   even_nat_def: "even (x::nat) == even (int x)"
 
+abbreviation
+  odd :: "'a::even_odd => bool"
+  "odd x == \<not> even x"
+
 
 subsection {* Even and odd are mutually exclusive *}
 
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -229,7 +229,7 @@
   "s =e> t == (s, t) \<in> par_eta"
 
 abbreviation (xsymbols)
-  par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
+  par_eta_red1 :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
   "op \<Rightarrow>\<^sub>\<eta> == op =e>"
 
 inductive par_eta
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -63,9 +63,9 @@
   "s ->> t == (s, t) \<in> beta^*"
 
 abbreviation (latex)
-  beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+  beta_red1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
   "op \<rightarrow>\<^sub>\<beta> == op ->"
-  beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
+  beta_reds1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
   "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
 
 inductive beta
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Lambda/Type.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -16,12 +16,12 @@
   "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
 
 abbreviation (xsymbols)
-  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+  shift1  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   "e\<langle>i:a\<rangle> == e<i:a>"
 
 abbreviation (HTML output)
-  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-  "shift == xsymbols.shift"
+  shift2  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+  "shift2 == shift"
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   by (simp add: shift_def)
@@ -63,13 +63,13 @@
   "env ||- ts : Ts == typings env ts Ts"
 
 abbreviation (xsymbols)
-  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+  typing_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   "env \<turnstile> t : T == env |- t : T"
 
 abbreviation (latex)
-  funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
+  funs2 :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
   "op \<Rrightarrow> == op =>>"
-  typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
+  typings_rel2 :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
   "env \<tturnstile> ts : Ts == env ||- ts : Ts"
 
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -366,7 +366,7 @@
   "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
 
 abbreviation (xsymbols)
-  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
+  rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
 
 inductive rtyping
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Library/Permutation.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -11,10 +11,9 @@
 consts
   perm :: "('a list * 'a list) set"
 
-syntax
-  "_perm" :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
-translations
-  "x <~~> y" == "(x, y) \<in> perm"
+abbreviation
+  perm_rel :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
+  "x <~~> y == (x, y) \<in> perm"
 
 inductive perm
   intros
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Library/SetsAndFunctions.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -58,21 +58,15 @@
   elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
   "a *o B == {c. EX b:B. c = a * b}"
 
-syntax
-  "elt_set_eq" :: "'a => 'a set => bool"      (infix "=o" 50)
-
-translations
-  "x =o A" => "x : A"
+abbreviation (inout)
+  elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
+  "x =o A == x : A"
 
 instance fun :: (type,semigroup_add)semigroup_add
-  apply intro_classes
-  apply (auto simp add: func_plus add_assoc)
-done
+  by default (auto simp add: func_plus add_assoc)
 
 instance fun :: (type,comm_monoid_add)comm_monoid_add
-  apply intro_classes
-  apply (auto simp add: func_zero func_plus add_ac)
-done
+  by default (auto simp add: func_zero func_plus add_ac)
 
 instance fun :: (type,ab_group_add)ab_group_add
   apply intro_classes
@@ -350,7 +344,8 @@
   apply auto
 done
 
-theorems set_times_plus_distribs = set_times_plus_distrib
+theorems set_times_plus_distribs =
+  set_times_plus_distrib
   set_times_plus_distrib2
 
 lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==> 
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/W0/W0.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -382,11 +382,9 @@
 consts
   has_type :: "(typ list \<times> expr \<times> typ) set"
 
-syntax
-  "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
-    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
-translations
-  "a |- e :: t" == "(a, e, t) \<in> has_type"
+abbreviation
+  has_type_rel  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
+  "a |- e :: t == (a, e, t) \<in> has_type"
 
 inductive has_type
   intros
diff -r c8cf1544b5a7 -r b808efaa5828 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -93,10 +93,9 @@
   Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<exists>" 10)
   "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
 
-syntax
-  "_not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
-translations
-  "x \<noteq> y"  \<rightleftharpoons>  "\<not> (x = y)"
+abbreviation
+  not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
+  "x \<noteq> y \<equiv> \<not> (x = y)"
 
 theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
 proof (unfold false_def)