tuned syntax/abbreviations;
authorwenzelm
Sun Apr 09 18:51:13 2006 +0200 (2006-04-09)
changeset 19380b808efaa5828
parent 19379 c8cf1544b5a7
child 19381 6cd8abc7f15b
tuned syntax/abbreviations;
src/FOL/IFOL.thy
src/HOL/Algebra/Coset.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Numeral.thy
src/HOL/Integ/Parity.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/W0/W0.thy
src/HOL/ex/Higher_Order_Logic.thy
     1.1 --- a/src/FOL/IFOL.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -50,12 +50,12 @@
     1.4    "x ~= y == ~ (x = y)"
     1.5  
     1.6  abbreviation (xsymbols)
     1.7 -  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
     1.8 +  not_equal1  (infixl "\<noteq>" 50)
     1.9    "x \<noteq> y == ~ (x = y)"
    1.10  
    1.11  abbreviation (HTML output)
    1.12 -  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.13 -  "not_equal == xsymbols.not_equal"
    1.14 +  not_equal2  (infixl "\<noteq>" 50)
    1.15 +  "not_equal2 == not_equal"
    1.16  
    1.17  syntax (xsymbols)
    1.18    Not           :: "o => o"                     ("\<not> _" [40] 40)
     2.1 --- a/src/HOL/Algebra/Coset.thy	Sun Apr 09 18:51:11 2006 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Apr 09 18:51:13 2006 +0200
     2.3 @@ -27,12 +27,9 @@
     2.4  locale normal = subgroup + group +
     2.5    assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
     2.6  
     2.7 -
     2.8 -syntax
     2.9 -  "@normal" :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
    2.10 -
    2.11 -translations
    2.12 -  "H \<lhd> G" == "normal H G"
    2.13 +abbreviation
    2.14 +  normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
    2.15 +  "H \<lhd> G \<equiv> normal H G"
    2.16  
    2.17  
    2.18  subsection {*Basic Properties of Cosets*}
     3.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Sun Apr 09 18:51:11 2006 +0200
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Sun Apr 09 18:51:13 2006 +0200
     3.3 @@ -14,8 +14,9 @@
     3.4  
     3.5  types hypreal = "real star"
     3.6  
     3.7 -syntax hypreal_of_real :: "real => real star"
     3.8 -translations "hypreal_of_real" => "star_of :: real => real star"
     3.9 +abbreviation
    3.10 +  hypreal_of_real :: "real => real star"
    3.11 +  "hypreal_of_real == star_of"
    3.12  
    3.13  constdefs
    3.14  
     4.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Sun Apr 09 18:51:11 2006 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Sun Apr 09 18:51:13 2006 +0200
     4.3 @@ -13,8 +13,9 @@
     4.4  
     4.5  types hypnat = "nat star"
     4.6  
     4.7 -syntax hypnat_of_nat :: "nat => nat star"
     4.8 -translations "hypnat_of_nat" => "star_of :: nat => nat star"
     4.9 +abbreviation
    4.10 +  hypnat_of_nat :: "nat => nat star"
    4.11 +  "hypnat_of_nat == star_of"
    4.12  
    4.13  subsection{*Properties Transferred from Naturals*}
    4.14  
     5.1 --- a/src/HOL/Integ/NatBin.thy	Sun Apr 09 18:51:11 2006 +0200
     5.2 +++ b/src/HOL/Integ/NatBin.thy	Sun Apr 09 18:51:13 2006 +0200
     5.3 @@ -18,7 +18,19 @@
     5.4  
     5.5  defs (overloaded)
     5.6    nat_number_of_def:
     5.7 -     "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
     5.8 +  "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
     5.9 +
    5.10 +abbreviation (xsymbols)
    5.11 +  square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
    5.12 +  "x\<twosuperior> == x^2"
    5.13 +
    5.14 +abbreviation (latex output)
    5.15 +  square1  ("(_\<twosuperior>)" [1000] 999)
    5.16 +  "square1 x == x^2"
    5.17 +
    5.18 +abbreviation (HTML output)
    5.19 +  square2  ("(_\<twosuperior>)" [1000] 999)
    5.20 +  "square2 x == x^2"
    5.21  
    5.22  
    5.23  subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
     6.1 --- a/src/HOL/Integ/Numeral.thy	Sun Apr 09 18:51:11 2006 +0200
     6.2 +++ b/src/HOL/Integ/Numeral.thy	Sun Apr 09 18:51:13 2006 +0200
     6.3 @@ -11,11 +11,6 @@
     6.4  uses "../Tools/numeral_syntax.ML"
     6.5  begin
     6.6  
     6.7 -text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
     6.8 -   Only qualified access Numeral.Pls and Numeral.Min is allowed.
     6.9 -   The datatype constructors bit.B0 and bit.B1 are similarly hidden.
    6.10 -   We do not hide Bit because we need the BIT infix syntax.*}
    6.11 -
    6.12  text{*This formalization defines binary arithmetic in terms of the integers
    6.13  rather than using a datatype. This avoids multiple representations (leading
    6.14  zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
    6.15 @@ -58,26 +53,12 @@
    6.16  
    6.17  syntax
    6.18    "_Numeral" :: "num_const => 'a"    ("_")
    6.19 -  Numeral0 :: 'a
    6.20 -  Numeral1 :: 'a
    6.21 -
    6.22 -translations
    6.23 -  "Numeral0" == "number_of Numeral.Pls"
    6.24 -  "Numeral1" == "number_of (Numeral.Pls BIT bit.B1)"
    6.25 -
    6.26  
    6.27  setup NumeralSyntax.setup
    6.28  
    6.29 -syntax (xsymbols)
    6.30 -  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
    6.31 -syntax (HTML output)
    6.32 -  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
    6.33 -syntax (output)
    6.34 -  "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
    6.35 -translations
    6.36 -  "x\<twosuperior>" == "x^2"
    6.37 -  "x\<twosuperior>" <= "x^(2::nat)"
    6.38 -
    6.39 +abbreviation
    6.40 +  "Numeral0 == number_of Pls"
    6.41 +  "Numeral1 == number_of (Pls BIT B1)"
    6.42  
    6.43  lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
    6.44    -- {* Unfold all @{text let}s involving constants *}
    6.45 @@ -112,90 +93,90 @@
    6.46         Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
    6.47  
    6.48  text{*Removal of leading zeroes*}
    6.49 -lemma Pls_0_eq [simp]: "Numeral.Pls BIT bit.B0 = Numeral.Pls"
    6.50 +lemma Pls_0_eq [simp]: "Pls BIT B0 = Pls"
    6.51  by (simp add: Bin_simps)
    6.52  
    6.53 -lemma Min_1_eq [simp]: "Numeral.Min BIT bit.B1 = Numeral.Min"
    6.54 +lemma Min_1_eq [simp]: "Min BIT B1 = Min"
    6.55  by (simp add: Bin_simps)
    6.56  
    6.57  subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
    6.58  
    6.59 -lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1"
    6.60 +lemma bin_succ_Pls [simp]: "bin_succ Pls = Pls BIT B1"
    6.61  by (simp add: Bin_simps) 
    6.62  
    6.63 -lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
    6.64 +lemma bin_succ_Min [simp]: "bin_succ Min = Pls"
    6.65  by (simp add: Bin_simps) 
    6.66  
    6.67 -lemma bin_succ_1 [simp]: "bin_succ(w BIT bit.B1) = (bin_succ w) BIT bit.B0"
    6.68 +lemma bin_succ_1 [simp]: "bin_succ(w BIT B1) = (bin_succ w) BIT B0"
    6.69  by (simp add: Bin_simps add_ac) 
    6.70  
    6.71 -lemma bin_succ_0 [simp]: "bin_succ(w BIT bit.B0) = w BIT bit.B1"
    6.72 +lemma bin_succ_0 [simp]: "bin_succ(w BIT B0) = w BIT B1"
    6.73  by (simp add: Bin_simps add_ac) 
    6.74  
    6.75 -lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
    6.76 +lemma bin_pred_Pls [simp]: "bin_pred Pls = Min"
    6.77  by (simp add: Bin_simps) 
    6.78  
    6.79 -lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT bit.B0"
    6.80 +lemma bin_pred_Min [simp]: "bin_pred Min = Min BIT B0"
    6.81  by (simp add: Bin_simps diff_minus) 
    6.82  
    6.83 -lemma bin_pred_1 [simp]: "bin_pred(w BIT bit.B1) = w BIT bit.B0"
    6.84 +lemma bin_pred_1 [simp]: "bin_pred(w BIT B1) = w BIT B0"
    6.85  by (simp add: Bin_simps) 
    6.86  
    6.87 -lemma bin_pred_0 [simp]: "bin_pred(w BIT bit.B0) = (bin_pred w) BIT bit.B1"
    6.88 +lemma bin_pred_0 [simp]: "bin_pred(w BIT B0) = (bin_pred w) BIT B1"
    6.89  by (simp add: Bin_simps diff_minus add_ac) 
    6.90  
    6.91 -lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
    6.92 +lemma bin_minus_Pls [simp]: "bin_minus Pls = Pls"
    6.93  by (simp add: Bin_simps) 
    6.94  
    6.95 -lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT bit.B1"
    6.96 +lemma bin_minus_Min [simp]: "bin_minus Min = Pls BIT B1"
    6.97  by (simp add: Bin_simps) 
    6.98  
    6.99  lemma bin_minus_1 [simp]:
   6.100 -     "bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1"
   6.101 +     "bin_minus (w BIT B1) = bin_pred (bin_minus w) BIT B1"
   6.102  by (simp add: Bin_simps add_ac diff_minus) 
   6.103  
   6.104 - lemma bin_minus_0 [simp]: "bin_minus(w BIT bit.B0) = (bin_minus w) BIT bit.B0"
   6.105 + lemma bin_minus_0 [simp]: "bin_minus(w BIT B0) = (bin_minus w) BIT B0"
   6.106  by (simp add: Bin_simps) 
   6.107  
   6.108  
   6.109  subsection{*Binary Addition and Multiplication:
   6.110           @{term bin_add} and @{term bin_mult}*}
   6.111  
   6.112 -lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
   6.113 +lemma bin_add_Pls [simp]: "bin_add Pls w = w"
   6.114  by (simp add: Bin_simps) 
   6.115  
   6.116 -lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
   6.117 +lemma bin_add_Min [simp]: "bin_add Min w = bin_pred w"
   6.118  by (simp add: Bin_simps diff_minus add_ac) 
   6.119  
   6.120  lemma bin_add_BIT_11 [simp]:
   6.121 -     "bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0"
   6.122 +     "bin_add (v BIT B1) (w BIT B1) = bin_add v (bin_succ w) BIT B0"
   6.123  by (simp add: Bin_simps add_ac)
   6.124  
   6.125  lemma bin_add_BIT_10 [simp]:
   6.126 -     "bin_add (v BIT bit.B1) (w BIT bit.B0) = (bin_add v w) BIT bit.B1"
   6.127 +     "bin_add (v BIT B1) (w BIT B0) = (bin_add v w) BIT B1"
   6.128  by (simp add: Bin_simps add_ac)
   6.129  
   6.130  lemma bin_add_BIT_0 [simp]:
   6.131 -     "bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y"
   6.132 +     "bin_add (v BIT B0) (w BIT y) = bin_add v w BIT y"
   6.133  by (simp add: Bin_simps add_ac)
   6.134  
   6.135 -lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
   6.136 +lemma bin_add_Pls_right [simp]: "bin_add w Pls = w"
   6.137  by (simp add: Bin_simps) 
   6.138  
   6.139 -lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
   6.140 +lemma bin_add_Min_right [simp]: "bin_add w Min = bin_pred w"
   6.141  by (simp add: Bin_simps diff_minus) 
   6.142  
   6.143 -lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
   6.144 +lemma bin_mult_Pls [simp]: "bin_mult Pls w = Pls"
   6.145  by (simp add: Bin_simps) 
   6.146  
   6.147 -lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
   6.148 +lemma bin_mult_Min [simp]: "bin_mult Min w = bin_minus w"
   6.149  by (simp add: Bin_simps) 
   6.150  
   6.151  lemma bin_mult_1 [simp]:
   6.152 -     "bin_mult (v BIT bit.B1) w = bin_add ((bin_mult v w) BIT bit.B0) w"
   6.153 +     "bin_mult (v BIT B1) w = bin_add ((bin_mult v w) BIT B0) w"
   6.154  by (simp add: Bin_simps add_ac left_distrib)
   6.155  
   6.156 -lemma bin_mult_0 [simp]: "bin_mult (v BIT bit.B0) w = (bin_mult v w) BIT bit.B0"
   6.157 +lemma bin_mult_0 [simp]: "bin_mult (v BIT B0) w = (bin_mult v w) BIT B0"
   6.158  by (simp add: Bin_simps left_distrib)
   6.159  
   6.160  
   6.161 @@ -228,7 +209,7 @@
   6.162  text{*The correctness of shifting.  But it doesn't seem to give a measurable
   6.163    speed-up.*}
   6.164  lemma double_number_of_BIT:
   6.165 -     "(1+1) * number_of w = (number_of (w BIT bit.B0) ::'a::number_ring)"
   6.166 +     "(1+1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
   6.167  by (simp add: number_of_eq Bin_simps left_distrib) 
   6.168  
   6.169  text{*Converting numerals 0 and 1 to their abstract versions*}
   6.170 @@ -264,14 +245,14 @@
   6.171  by (simp add: diff_minus number_of_add number_of_minus)
   6.172  
   6.173  
   6.174 -lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
   6.175 +lemma number_of_Pls: "number_of Pls = (0::'a::number_ring)"
   6.176  by (simp add: number_of_eq Bin_simps) 
   6.177  
   6.178 -lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
   6.179 +lemma number_of_Min: "number_of Min = (- 1::'a::number_ring)"
   6.180  by (simp add: number_of_eq Bin_simps) 
   6.181  
   6.182  lemma number_of_BIT:
   6.183 -     "number_of(w BIT x) = (case x of bit.B0 => 0 | bit.B1 => (1::'a::number_ring)) +
   6.184 +     "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring)) +
   6.185  	                   (number_of w) + (number_of w)"
   6.186  by (simp add: number_of_eq Bin_simps split: bit.split) 
   6.187  
   6.188 @@ -286,10 +267,10 @@
   6.189     iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
   6.190  by (simp add: iszero_def compare_rls number_of_add number_of_minus)
   6.191  
   6.192 -lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
   6.193 +lemma iszero_number_of_Pls: "iszero ((number_of Pls)::'a::number_ring)"
   6.194  by (simp add: iszero_def numeral_0_eq_0)
   6.195  
   6.196 -lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
   6.197 +lemma nonzero_number_of_Min: "~ iszero ((number_of Min)::'a::number_ring)"
   6.198  by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
   6.199  
   6.200  
   6.201 @@ -353,17 +334,17 @@
   6.202  
   6.203  lemma iszero_number_of_BIT:
   6.204       "iszero (number_of (w BIT x)::'a) = 
   6.205 -      (x=bit.B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
   6.206 +      (x=B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
   6.207  by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
   6.208                Ints_odd_nonzero Ints_def split: bit.split)
   6.209  
   6.210  lemma iszero_number_of_0:
   6.211 -     "iszero (number_of (w BIT bit.B0) :: 'a::{ordered_idom,number_ring}) = 
   6.212 +     "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
   6.213        iszero (number_of w :: 'a)"
   6.214  by (simp only: iszero_number_of_BIT simp_thms)
   6.215  
   6.216  lemma iszero_number_of_1:
   6.217 -     "~ iszero (number_of (w BIT bit.B1)::'a::{ordered_idom,number_ring})"
   6.218 +     "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
   6.219  by (simp add: iszero_number_of_BIT) 
   6.220  
   6.221  
   6.222 @@ -377,13 +358,13 @@
   6.223  done
   6.224  
   6.225  text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
   6.226 -  @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
   6.227 +  @{term Numeral0} IS @{term "number_of Pls"} *}
   6.228  lemma not_neg_number_of_Pls:
   6.229 -     "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
   6.230 +     "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
   6.231  by (simp add: neg_def numeral_0_eq_0)
   6.232  
   6.233  lemma neg_number_of_Min:
   6.234 -     "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
   6.235 +     "neg (number_of Min ::'a::{ordered_idom,number_ring})"
   6.236  by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
   6.237  
   6.238  lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
   6.239 @@ -511,4 +492,7 @@
   6.240  apply (simp only: compare_rls)
   6.241  done
   6.242  
   6.243 +
   6.244 +hide (open) const Pls Min B0 B1
   6.245 +
   6.246  end
     7.1 --- a/src/HOL/Integ/Parity.thy	Sun Apr 09 18:51:11 2006 +0200
     7.2 +++ b/src/HOL/Integ/Parity.thy	Sun Apr 09 18:51:13 2006 +0200
     7.3 @@ -11,22 +11,20 @@
     7.4  
     7.5  axclass even_odd < type
     7.6  
     7.7 -instance int :: even_odd ..
     7.8 -instance nat :: even_odd ..
     7.9 -
    7.10  consts
    7.11    even :: "'a::even_odd => bool"
    7.12  
    7.13 -syntax 
    7.14 -  odd :: "'a::even_odd => bool"
    7.15 -
    7.16 -translations 
    7.17 -  "odd x" == "~even x" 
    7.18 +instance int :: even_odd ..
    7.19 +instance nat :: even_odd ..
    7.20  
    7.21  defs (overloaded)
    7.22    even_def: "even (x::int) == x mod 2 = 0"
    7.23    even_nat_def: "even (x::nat) == even (int x)"
    7.24  
    7.25 +abbreviation
    7.26 +  odd :: "'a::even_odd => bool"
    7.27 +  "odd x == \<not> even x"
    7.28 +
    7.29  
    7.30  subsection {* Even and odd are mutually exclusive *}
    7.31  
     8.1 --- a/src/HOL/Lambda/Eta.thy	Sun Apr 09 18:51:11 2006 +0200
     8.2 +++ b/src/HOL/Lambda/Eta.thy	Sun Apr 09 18:51:13 2006 +0200
     8.3 @@ -229,7 +229,7 @@
     8.4    "s =e> t == (s, t) \<in> par_eta"
     8.5  
     8.6  abbreviation (xsymbols)
     8.7 -  par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
     8.8 +  par_eta_red1 :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
     8.9    "op \<Rightarrow>\<^sub>\<eta> == op =e>"
    8.10  
    8.11  inductive par_eta
     9.1 --- a/src/HOL/Lambda/Lambda.thy	Sun Apr 09 18:51:11 2006 +0200
     9.2 +++ b/src/HOL/Lambda/Lambda.thy	Sun Apr 09 18:51:13 2006 +0200
     9.3 @@ -63,9 +63,9 @@
     9.4    "s ->> t == (s, t) \<in> beta^*"
     9.5  
     9.6  abbreviation (latex)
     9.7 -  beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
     9.8 +  beta_red1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
     9.9    "op \<rightarrow>\<^sub>\<beta> == op ->"
    9.10 -  beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    9.11 +  beta_reds1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    9.12    "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
    9.13  
    9.14  inductive beta
    10.1 --- a/src/HOL/Lambda/Type.thy	Sun Apr 09 18:51:11 2006 +0200
    10.2 +++ b/src/HOL/Lambda/Type.thy	Sun Apr 09 18:51:13 2006 +0200
    10.3 @@ -16,12 +16,12 @@
    10.4    "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
    10.5  
    10.6  abbreviation (xsymbols)
    10.7 -  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    10.8 +  shift1  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    10.9    "e\<langle>i:a\<rangle> == e<i:a>"
   10.10  
   10.11  abbreviation (HTML output)
   10.12 -  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   10.13 -  "shift == xsymbols.shift"
   10.14 +  shift2  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   10.15 +  "shift2 == shift"
   10.16  
   10.17  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   10.18    by (simp add: shift_def)
   10.19 @@ -63,13 +63,13 @@
   10.20    "env ||- ts : Ts == typings env ts Ts"
   10.21  
   10.22  abbreviation (xsymbols)
   10.23 -  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   10.24 +  typing_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   10.25    "env \<turnstile> t : T == env |- t : T"
   10.26  
   10.27  abbreviation (latex)
   10.28 -  funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
   10.29 +  funs2 :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
   10.30    "op \<Rrightarrow> == op =>>"
   10.31 -  typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
   10.32 +  typings_rel2 :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
   10.33      ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
   10.34    "env \<tturnstile> ts : Ts == env ||- ts : Ts"
   10.35  
    11.1 --- a/src/HOL/Lambda/WeakNorm.thy	Sun Apr 09 18:51:11 2006 +0200
    11.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Sun Apr 09 18:51:13 2006 +0200
    11.3 @@ -366,7 +366,7 @@
    11.4    "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
    11.5  
    11.6  abbreviation (xsymbols)
    11.7 -  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
    11.8 +  rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
    11.9    "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
   11.10  
   11.11  inductive rtyping
    12.1 --- a/src/HOL/Library/Permutation.thy	Sun Apr 09 18:51:11 2006 +0200
    12.2 +++ b/src/HOL/Library/Permutation.thy	Sun Apr 09 18:51:13 2006 +0200
    12.3 @@ -11,10 +11,9 @@
    12.4  consts
    12.5    perm :: "('a list * 'a list) set"
    12.6  
    12.7 -syntax
    12.8 -  "_perm" :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
    12.9 -translations
   12.10 -  "x <~~> y" == "(x, y) \<in> perm"
   12.11 +abbreviation
   12.12 +  perm_rel :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
   12.13 +  "x <~~> y == (x, y) \<in> perm"
   12.14  
   12.15  inductive perm
   12.16    intros
    13.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Sun Apr 09 18:51:11 2006 +0200
    13.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Sun Apr 09 18:51:13 2006 +0200
    13.3 @@ -58,21 +58,15 @@
    13.4    elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
    13.5    "a *o B == {c. EX b:B. c = a * b}"
    13.6  
    13.7 -syntax
    13.8 -  "elt_set_eq" :: "'a => 'a set => bool"      (infix "=o" 50)
    13.9 -
   13.10 -translations
   13.11 -  "x =o A" => "x : A"
   13.12 +abbreviation (inout)
   13.13 +  elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
   13.14 +  "x =o A == x : A"
   13.15  
   13.16  instance fun :: (type,semigroup_add)semigroup_add
   13.17 -  apply intro_classes
   13.18 -  apply (auto simp add: func_plus add_assoc)
   13.19 -done
   13.20 +  by default (auto simp add: func_plus add_assoc)
   13.21  
   13.22  instance fun :: (type,comm_monoid_add)comm_monoid_add
   13.23 -  apply intro_classes
   13.24 -  apply (auto simp add: func_zero func_plus add_ac)
   13.25 -done
   13.26 +  by default (auto simp add: func_zero func_plus add_ac)
   13.27  
   13.28  instance fun :: (type,ab_group_add)ab_group_add
   13.29    apply intro_classes
   13.30 @@ -350,7 +344,8 @@
   13.31    apply auto
   13.32  done
   13.33  
   13.34 -theorems set_times_plus_distribs = set_times_plus_distrib
   13.35 +theorems set_times_plus_distribs =
   13.36 +  set_times_plus_distrib
   13.37    set_times_plus_distrib2
   13.38  
   13.39  lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==> 
    14.1 --- a/src/HOL/W0/W0.thy	Sun Apr 09 18:51:11 2006 +0200
    14.2 +++ b/src/HOL/W0/W0.thy	Sun Apr 09 18:51:13 2006 +0200
    14.3 @@ -382,11 +382,9 @@
    14.4  consts
    14.5    has_type :: "(typ list \<times> expr \<times> typ) set"
    14.6  
    14.7 -syntax
    14.8 -  "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
    14.9 -    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
   14.10 -translations
   14.11 -  "a |- e :: t" == "(a, e, t) \<in> has_type"
   14.12 +abbreviation
   14.13 +  has_type_rel  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
   14.14 +  "a |- e :: t == (a, e, t) \<in> has_type"
   14.15  
   14.16  inductive has_type
   14.17    intros
    15.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Sun Apr 09 18:51:11 2006 +0200
    15.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Sun Apr 09 18:51:13 2006 +0200
    15.3 @@ -93,10 +93,9 @@
    15.4    Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<exists>" 10)
    15.5    "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
    15.6  
    15.7 -syntax
    15.8 -  "_not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
    15.9 -translations
   15.10 -  "x \<noteq> y"  \<rightleftharpoons>  "\<not> (x = y)"
   15.11 +abbreviation
   15.12 +  not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
   15.13 +  "x \<noteq> y \<equiv> \<not> (x = y)"
   15.14  
   15.15  theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
   15.16  proof (unfold false_def)