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)