--- a/NEWS Sat Apr 08 22:12:02 2006 +0200
+++ b/NEWS Sat Apr 08 22:51:06 2006 +0200
@@ -144,9 +144,9 @@
eq (infix "===" 50)
where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
- abbreviation (output)
+ abbreviation
neq (infix "=!=" 50)
- "(x =!= y) <-> ~ (x === y)"
+ "x =!= y == ~ (x === y)"
These specifications may be also used in a locale context. Then the
constants being introduced depend on certain fixed parameters, and the
@@ -157,10 +157,9 @@
entities from a monomorphic theory.
Presently, abbreviations are only available 'in' a target locale, but
-not inherited by general import expressions.
-
-Also note that 'abbreviation' may be used as a type-safe replacement
-for 'syntax' + 'translations' in common applications.
+not inherited by general import expressions. Also note that
+'abbreviation' may be used as a type-safe replacement for 'syntax' +
+'translations' in common applications.
* Provers/induct: improved internal context management to support
local fixes and defines on-the-fly. Thus explicit meta-level
--- a/doc-src/IsarRef/generic.tex Sat Apr 08 22:12:02 2006 +0200
+++ b/doc-src/IsarRef/generic.tex Sat Apr 08 22:51:06 2006 +0200
@@ -24,7 +24,7 @@
'definition' locale? (constdecl? constdef +)
;
- 'abbreviation' locale? '(output)'? (constdecl? prop +)
+ 'abbreviation' locale? mode? (constdecl? prop +)
;
'axiomatization' locale? consts? ('where' specs)?
;
@@ -55,16 +55,20 @@
supported here.
\item $\isarkeyword{abbreviation}~c~\isarkeyword{where}~eq$ introduces
- a syntactic constant which is associated with a certain term derived
- from the specification given as $eq$. The very same transformations
- as for $\isarkeyword{definition}$ are applied here, although
- additional conditions are not supported.
+ a syntactic constant which is associated with a certain term
+ according to the meta-level equality $eq$.
Abbreviations participate in the usual type-inference process, but
- are expanded before the logic ever sees them. The expansion is
- one-way by default; the ``$(output)$'' option makes abbreviations
- fold back whenever terms are pretty printed. The latter needs some
- care to avoid overlapping or looping syntactic replacements!
+ are expanded before the logic ever sees them. Pretty printing of
+ terms involves higher-order rewriting with rules stemming from
+ reverted abbreviations. This needs some care to avoid overlapping
+ or looping syntactic replacements!
+
+ The optional $mode$ specification restricts output to a particular
+ print mode; using ``$input$'' here achieves the effect of one-way
+ abbreviations. The mode may also include an ``$output$'' qualifier
+ that affects the concrete syntax declared for abbreviations, cf.\
+ $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
\item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
\isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants
--- a/src/FOL/IFOL.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/FOL/IFOL.thy Sat Apr 08 22:51:06 2006 +0200
@@ -45,10 +45,18 @@
Ex1 :: "('a => o) => o" (binder "EX! " 10)
-abbreviation (output)
+abbreviation
not_equal :: "['a, 'a] => o" (infixl "~=" 50)
"x ~= y == ~ (x = y)"
+abbreviation (xsymbols)
+ not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+ "x \<noteq> y == ~ (x = y)"
+
+abbreviation (HTML output)
+ not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+ "not_equal == xsymbols.not_equal"
+
syntax (xsymbols)
Not :: "o => o" ("\<not> _" [40] 40)
"op &" :: "[o, o] => o" (infixr "\<and>" 35)
@@ -56,7 +64,6 @@
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
"op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
"op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
@@ -67,7 +74,6 @@
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
local
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Sat Apr 08 22:51:06 2006 +0200
@@ -19,9 +19,9 @@
subsubsection{*a little abbreviation*}
-syntax Ciph :: "agent => msg"
-
-translations "Ciph A X" == "Crypt (shrK A) X"
+abbreviation
+ Ciph :: "agent => msg => msg"
+ "Ciph A X == Crypt (shrK A) X"
subsubsection{*agent associated to a key*}
--- a/src/HOL/Equiv_Relations.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Equiv_Relations.thy Sat Apr 08 22:51:06 2006 +0200
@@ -163,9 +163,9 @@
fixes r and f
assumes congruent: "(y,z) \<in> r ==> f y = f z"
-abbreviation (output)
+abbreviation
RESPECTS :: "('a => 'b) => ('a * 'a) set => bool" (infixr "respects" 80)
- "f respects r = congruent r f"
+ "f respects r == congruent r f"
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
--- a/src/HOL/Finite_Set.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Finite_Set.thy Sat Apr 08 22:51:06 2006 +0200
@@ -13,8 +13,8 @@
subsection {* Definition and basic properties *}
consts Finites :: "'a set set"
-abbreviation (output)
- "finite A = (A : Finites)"
+abbreviation
+ "finite A == A : Finites"
inductive Finites
intros
--- a/src/HOL/Fun.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Fun.thy Sat Apr 08 22:51:06 2006 +0200
@@ -59,19 +59,19 @@
constdefs
inj_on :: "['a => 'b, 'a set] => bool" (*injective*)
- "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+ "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
text{*A common special case: functions injective over the entire domain type.*}
-abbreviation (output)
- "inj f = inj_on f UNIV"
+abbreviation
+ "inj f == inj_on f UNIV"
constdefs
surj :: "('a => 'b) => bool" (*surjective*)
- "surj f == ! y. ? x. y=f(x)"
+ "surj f == ! y. ? x. y=f(x)"
bij :: "('a => 'b) => bool" (*bijective*)
- "bij f == inj f & surj f"
+ "bij f == inj f & surj f"
--- a/src/HOL/Infinite_Set.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Infinite_Set.thy Sat Apr 08 22:51:06 2006 +0200
@@ -13,12 +13,9 @@
text {* Some elementary facts about infinite sets, by Stefan Merz. *}
-syntax infinite :: "'a set \<Rightarrow> bool"
-translations "infinite S" == "\<not> finite S"
-(* doesnt work:
-abbreviation (output)
- "infinite S = (\<not> finite S)"
-*)
+abbreviation
+ infinite :: "'a set \<Rightarrow> bool"
+ "infinite S == \<not> finite S"
text {*
Infinite sets are non-empty, and if we remove some elements
--- a/src/HOL/Isar_examples/Hoare.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy Sat Apr 08 22:51:06 2006 +0200
@@ -31,7 +31,7 @@
| Cond "'a bexp" "'a com" "'a com"
| While "'a bexp" "'a assn" "'a com"
-abbreviation (output)
+abbreviation
Skip ("SKIP")
"SKIP == Basic id"
--- a/src/HOL/Lambda/Commutation.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Commutation.thy Sat Apr 08 22:51:06 2006 +0200
@@ -25,9 +25,9 @@
"Church_Rosser R =
(\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
-abbreviation (output)
+abbreviation
confluent :: "('a \<times> 'a) set => bool"
- "confluent R = diamond (R^*)"
+ "confluent R == diamond (R^*)"
subsection {* Basic lemmas *}
--- a/src/HOL/Lambda/Eta.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy Sat Apr 08 22:51:06 2006 +0200
@@ -21,13 +21,13 @@
consts
eta :: "(dB \<times> dB) set"
-abbreviation (output)
+abbreviation
eta_red :: "[dB, dB] => bool" (infixl "-e>" 50)
- "(s -e> t) = ((s, t) \<in> eta)"
+ "s -e> t == (s, t) \<in> eta"
eta_reds :: "[dB, dB] => bool" (infixl "-e>>" 50)
- "(s -e>> t) = ((s, t) \<in> eta^*)"
+ "s -e>> t == (s, t) \<in> eta^*"
eta_red0 :: "[dB, dB] => bool" (infixl "-e>=" 50)
- "(s -e>= t) = ((s, t) \<in> eta^=)"
+ "s -e>= t == (s, t) \<in> eta^="
inductive eta
intros
@@ -224,12 +224,13 @@
consts
par_eta :: "(dB \<times> dB) set"
-abbreviation (output)
+abbreviation
par_eta_red :: "[dB, dB] => bool" (infixl "=e>" 50)
- "(s =e> t) = ((s, t) \<in> par_eta)"
+ "s =e> t == (s, t) \<in> par_eta"
-syntax (xsymbols)
+abbreviation (xsymbols)
par_eta_red :: "[dB, dB] => bool" (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
+ "op \<Rightarrow>\<^sub>\<eta> == op =e>"
inductive par_eta
intros
--- a/src/HOL/Lambda/Lambda.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Lambda.thy Sat Apr 08 22:51:06 2006 +0200
@@ -56,15 +56,17 @@
consts
beta :: "(dB \<times> dB) set"
-abbreviation (output)
+abbreviation
beta_red :: "[dB, dB] => bool" (infixl "->" 50)
- "(s -> t) = ((s, t) \<in> beta)"
+ "s -> t == (s, t) \<in> beta"
beta_reds :: "[dB, dB] => bool" (infixl "->>" 50)
- "(s ->> t) = ((s, t) \<in> beta^*)"
+ "s ->> t == (s, t) \<in> beta^*"
-syntax (latex)
+abbreviation (latex)
beta_red :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ "op \<rightarrow>\<^sub>\<beta> == op ->"
beta_reds :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
+ "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
inductive beta
intros
--- a/src/HOL/Lambda/ListApplication.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Sat Apr 08 22:51:06 2006 +0200
@@ -8,9 +8,9 @@
theory ListApplication imports Lambda begin
-abbreviation (output)
+abbreviation
list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150)
- "t \<degree>\<degree> ts = foldl (op \<degree>) t ts"
+ "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
by (induct ts rule: rev_induct) auto
--- a/src/HOL/Lambda/ListBeta.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Sat Apr 08 22:51:06 2006 +0200
@@ -12,9 +12,9 @@
Lifting beta-reduction to lists of terms, reducing exactly one element.
*}
-abbreviation (output)
+abbreviation
list_beta :: "dB list => dB list => bool" (infixl "=>" 50)
- "(rs => ss) = ((rs, ss) : step1 beta)"
+ "rs => ss == (rs, ss) : step1 beta"
lemma head_Var_reduction:
"Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
--- a/src/HOL/Lambda/ParRed.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/ParRed.thy Sat Apr 08 22:51:06 2006 +0200
@@ -17,9 +17,9 @@
consts
par_beta :: "(dB \<times> dB) set"
-abbreviation (output)
+abbreviation
par_beta_red :: "[dB, dB] => bool" (infixl "=>" 50)
- "(s => t) = ((s, t) \<in> par_beta)"
+ "s => t == (s, t) \<in> par_beta"
inductive par_beta
intros
--- a/src/HOL/Lambda/Type.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Type.thy Sat Apr 08 22:51:06 2006 +0200
@@ -14,10 +14,14 @@
definition
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91)
"e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
-syntax (xsymbols)
- shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-syntax (HTML output)
- shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+
+abbreviation (xsymbols)
+ shift ("_\<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"
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
by (simp add: shift_def)
@@ -47,23 +51,27 @@
typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
-abbreviation (output)
+abbreviation
funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200)
- "Ts =>> T = foldr Fun Ts T"
+ "Ts =>> T == foldr Fun Ts T"
typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50)
- "(env |- t : T) = ((env, t, T) \<in> typing)"
+ "env |- t : T == (env, t, T) \<in> typing"
typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
("_ ||- _ : _" [50, 50, 50] 50)
- "(env ||- ts : Ts) = typings env ts Ts"
+ "env ||- ts : Ts == typings env ts Ts"
-syntax (xsymbols)
+abbreviation (xsymbols)
typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-syntax (latex)
+ "env \<turnstile> t : T == env |- t : T"
+
+abbreviation (latex)
funs :: "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"
("_ \<tturnstile> _ : _" [50, 50, 50] 50)
+ "env \<tturnstile> ts : Ts == env ||- ts : Ts"
inductive typing
intros
--- a/src/HOL/Lambda/WeakNorm.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Sat Apr 08 22:51:06 2006 +0200
@@ -361,11 +361,13 @@
consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
-abbreviation (output)
+abbreviation
rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
- "(e |-\<^sub>R t : T) = ((e, t, T) \<in> rtyping)"
-syntax (xsymbols)
+ "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)
+ "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
inductive rtyping
intros
--- a/src/HOL/Library/Accessible_Part.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Library/Accessible_Part.thy Sat Apr 08 22:51:06 2006 +0200
@@ -23,7 +23,7 @@
intros
accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
-abbreviation (output)
+abbreviation
termi :: "('a \<times> 'a) set => 'a set"
"termi r == acc (r\<inverse>)"
--- a/src/HOL/Library/Multiset.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Apr 08 22:51:06 2006 +0200
@@ -33,9 +33,9 @@
MCollect :: "'a multiset => ('a => bool) => 'a multiset"
"MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
-abbreviation (output)
+abbreviation
Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50)
- "(a :# M) = (0 < count M a)"
+ "a :# M == 0 < count M a"
syntax
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})")
--- a/src/HOL/List.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/List.thy Sat Apr 08 22:51:06 2006 +0200
@@ -54,9 +54,9 @@
filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list"
-abbreviation (output)
- upto:: "nat => nat => nat list" ("(1[_../_])")
-"[i..j] = [i..<(Suc j)]"
+abbreviation
+ upto:: "nat => nat => nat list" ("(1[_../_])")
+ "[i..j] == [i..<(Suc j)]"
nonterminals lupdbinds lupdbind
@@ -93,9 +93,9 @@
Function @{text size} is overloaded for all datatypes. Users may
refer to the list version as @{text length}. *}
-abbreviation (output)
- length :: "'a list => nat"
-"length = size"
+abbreviation
+ length :: "'a list => nat"
+ "length == size"
primrec
"hd(x#xs) = x"
--- a/src/HOL/Relation.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Relation.thy Sat Apr 08 22:51:06 2006 +0200
@@ -58,9 +58,9 @@
inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
"inv_image r f == {(x, y). (f x, f y) : r}"
-abbreviation (output)
+abbreviation
reflexive :: "('a * 'a) set => bool" -- {* reflexivity over a type *}
- "reflexive = refl UNIV"
+ "reflexive == refl UNIV"
subsection {* The identity relation *}
--- a/src/HOL/Set.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Set.thy Sat Apr 08 22:51:06 2006 +0200
@@ -47,9 +47,9 @@
subsection {* Additional concrete syntax *}
-abbreviation (output)
+abbreviation
range :: "('a => 'b) => 'b set" -- "of function"
- "range f = f ` UNIV"
+ "range f == f ` UNIV"
syntax
"op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership"
--- a/src/HOL/Unix/Unix.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Unix/Unix.thy Sat Apr 08 22:51:06 2006 +0200
@@ -352,11 +352,9 @@
consts
transition :: "(file \<times> operation \<times> file) set"
-syntax
- "_transition" :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
- ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
-translations
- "root \<midarrow>x\<rightarrow> root'" \<rightleftharpoons> "(root, x, root') \<in> transition"
+abbreviation
+ transition_rel ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
+ "root \<midarrow>x\<rightarrow> root' \<equiv> (root, x, root') \<in> transition"
inductive transition
intros
@@ -510,11 +508,9 @@
consts
transitions :: "(file \<times> operation list \<times> file) set"
-syntax
- "_transitions" :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
- ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
-translations
- "root =xs\<Rightarrow> root'" \<rightleftharpoons> "(root, xs, root') \<in> transitions"
+abbreviation
+ transitions_rel ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
+ "root =xs\<Rightarrow> root' \<equiv> (root, xs, root') \<in> transitions"
inductive transitions
intros
--- a/src/HOL/ex/Abstract_NAT.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy Sat Apr 08 22:51:06 2006 +0200
@@ -37,8 +37,8 @@
Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
(succ m, r m n) \<in> REC zero succ e r"
-abbreviation (in NAT) (output)
- "Rec = REC zero succ"
+abbreviation (in NAT)
+ "Rec == REC zero succ"
lemma (in NAT) Rec_functional:
fixes x :: 'n
--- a/src/HOL/ex/Classpackage.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy Sat Apr 08 22:51:06 2006 +0200
@@ -150,7 +150,7 @@
abbreviation (in monoid)
abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
- "(x \<^loc>\<up> n) = npow n x"
+ "x \<^loc>\<up> n == npow n x"
lemma (in monoid) npow_def:
"x \<^loc>\<up> 0 = \<^loc>\<one>"
@@ -290,7 +290,7 @@
abbreviation (in group)
abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
- "(x \<^loc>\<up> k) = pow k x"
+ "x \<^loc>\<up> k == pow k x"
lemma (in group) int_pow_zero:
"x \<^loc>\<up> (0::int) = \<^loc>\<one>"