--- 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)
--- 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*}
--- 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
--- 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*}
--- 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}*}
--- 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
--- 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 *}
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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 ==>
--- 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
--- 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)