--- a/src/CTT/CTT.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/CTT/CTT.thy Thu Apr 26 14:24:08 2007 +0200
@@ -37,7 +37,7 @@
(*General Product and Function Space*)
Prod :: "[t, i=>t]=>t"
(*Types*)
- "+" :: "[t,t]=>t" (infixr 40)
+ Plus :: "[t,t]=>t" (infixr "+" 40)
(*Equality type*)
Eq :: "[t,i,i]=>t"
eq :: "i"
@@ -51,7 +51,7 @@
(*Functions*)
lambda :: "(i => i) => i" (binder "lam " 10)
- "`" :: "[i,i]=>i" (infixl 60)
+ app :: "[i,i]=>i" (infixl "`" 60)
(*Natural numbers*)
"0" :: "i" ("0")
(*Pairing*)
--- a/src/HOL/Algebra/abstract/Ring2.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Thu Apr 26 14:24:08 2007 +0200
@@ -15,7 +15,7 @@
text {* Most constants are already declared by HOL. *}
consts
- assoc :: "['a::times, 'a] => bool" (infixl 50)
+ assoc :: "['a::times, 'a] => bool" (infixl "assoc" 50)
irred :: "'a::{zero, one, times} => bool"
prime :: "'a::{zero, one, times} => bool"
--- a/src/HOL/Hyperreal/Poly.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Thu Apr 26 14:24:08 2007 +0200
@@ -23,20 +23,20 @@
subsection{*Arithmetic Operations on Polynomials*}
text{*addition*}
-consts "+++" :: "[real list, real list] => real list" (infixl 65)
+consts padd :: "[real list, real list] => real list" (infixl "+++" 65)
primrec
padd_Nil: "[] +++ l2 = l2"
padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
else (h + hd l2)#(t +++ tl l2))"
text{*Multiplication by a constant*}
-consts "%*" :: "[real, real list] => real list" (infixl 70)
+consts cmult :: "[real, real list] => real list" (infixl "%*" 70)
primrec
cmult_Nil: "c %* [] = []"
cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
text{*Multiplication by a polynomial*}
-consts "***" :: "[real list, real list] => real list" (infixl 70)
+consts pmult :: "[real list, real list] => real list" (infixl "***" 70)
primrec
pmult_Nil: "[] *** l2 = []"
pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
@@ -50,7 +50,7 @@
text{*Exponential*}
-consts "%^" :: "[real list, nat] => real list" (infixl 80)
+consts pexp :: "[real list, nat] => real list" (infixl "%^" 80)
primrec
pexp_0: "p %^ 0 = [1]"
pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
--- a/src/HOL/Nominal/Nominal.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Apr 26 14:24:08 2007 +0200
@@ -176,7 +176,7 @@
fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80)
"a \<sharp> x \<equiv> a \<notin> supp x"
- supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)
+ supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80)
"S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
lemma supp_fresh_iff:
@@ -1770,7 +1770,7 @@
and b: "S1 \<subseteq> S2"
shows "S2 supports x"
using a b
- by (force simp add: "op supports_def")
+ by (force simp add: supports_def)
lemma supp_is_subset:
fixes S :: "'x set"
@@ -1782,7 +1782,7 @@
assume "\<not>(supp x \<subseteq> S)"
hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
- from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
+ from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold supports_def, force)
hence "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by force
with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
hence "a\<notin>(supp x)" by (unfold supp_def, auto)
@@ -1794,7 +1794,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE ('x)"
shows "((supp x)::'x set) supports x"
-proof (unfold "op supports_def", intro strip)
+proof (unfold supports_def, intro strip)
fix a b
assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
@@ -1860,7 +1860,7 @@
and a: "\<forall>x\<in>X. (\<forall>(a::'x) (b::'x). a\<notin>S\<and>b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x)\<in>X)"
shows "S supports X"
using a
-apply(auto simp add: "op supports_def")
+apply(auto simp add: supports_def)
apply(simp add: pt_set_bij1a[OF pt, OF at])
apply(force simp add: pt_swap_bij[OF pt, OF at])
apply(simp add: pt_set_bij1a[OF pt, OF at])
@@ -1885,7 +1885,7 @@
shows "X supports X"
proof -
have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X" by (auto simp add: perm_set_def at_calc[OF at])
- then show ?thesis by (simp add: "op supports_def")
+ then show ?thesis by (simp add: supports_def)
qed
lemma infinite_Collection:
@@ -2076,7 +2076,7 @@
shows "supp (f x) \<subseteq> (((supp f)\<union>(supp x))::'x set)"
proof -
have s1: "((supp f)\<union>((supp x)::'x set)) supports (f x)"
- proof (simp add: "op supports_def", fold fresh_def, auto)
+ proof (simp add: supports_def, fold fresh_def, auto)
fix a::"'x" and b::"'x"
assume "a\<sharp>f" and "b\<sharp>f"
hence a1: "[(a,b)]\<bullet>f = f"
@@ -2171,7 +2171,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
- apply(simp add: "op supports_def" fresh_def[symmetric])
+ apply(simp add: supports_def fresh_def[symmetric])
apply(rule allI)+
apply(rule impI)
apply(erule conjE)
@@ -2592,7 +2592,7 @@
and f1: "finite ((supp h)::'x set)"
and a: "\<exists>(a::'x). a\<sharp>(h,h a)"
shows "((supp h)::'x set) supports (fresh_fun h)"
- apply(simp add: "op supports_def" fresh_def[symmetric])
+ apply(simp add: supports_def fresh_def[symmetric])
apply(auto)
apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a])
apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Apr 26 14:24:08 2007 +0200
@@ -55,7 +55,7 @@
val not_false = thm "not_False_eq_True"
val perm_fun_def = thm "Nominal.perm_fun_def"
val perm_eq_app = thm "Nominal.pt_fun_app_eq"
-val supports_def = thm "Nominal.op supports_def";
+val supports_def = thm "Nominal.supports_def";
val fresh_def = thm "Nominal.fresh_def";
val fresh_prod = thm "Nominal.fresh_prod";
val fresh_unit = thm "Nominal.fresh_unit";
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Thu Apr 26 14:24:08 2007 +0200
@@ -57,7 +57,7 @@
(* binary composition of action signatures and automata *)
asig_comp ::"['a signature, 'a signature] => 'a signature"
compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
- "||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10)
+ par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "||" 10)
(* hiding and restricting *)
hide_asig :: "['a signature, 'a set] => 'a signature"
@@ -86,7 +86,9 @@
"_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool"
("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
- "op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\<parallel>" 10)
+
+notation (xsymbols)
+ par (infixr "\<parallel>" 10)
inductive "reachable C"
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Thu Apr 26 14:24:08 2007 +0200
@@ -9,7 +9,7 @@
imports HOLCF
begin
-domain 'a seq = nil | "##" (HD :: 'a) (lazy TL :: "'a seq") (infixr 65)
+domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65)
consts
sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -30,14 +30,13 @@
nproj :: "nat => 'a seq => 'a"
sproj :: "nat => 'a seq => 'a seq"
-syntax
- "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65)
- "Finite" :: "'a seq => bool"
+abbreviation
+ sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) where
+ "xs @@ ys == sconc $ xs $ ys"
-translations
- "xs @@ ys" == "sconc $ xs $ ys"
- "Finite x" == "x:sfinite"
- "~(Finite x)" =="x~:sfinite"
+abbreviation
+ Finite :: "'a seq => bool" where
+ "Finite x == x:sfinite"
defs
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Thu Apr 26 14:24:08 2007 +0200
@@ -58,7 +58,7 @@
fairtraces ::"('a,'s)ioa => 'a trace set"
(* Notions of implementation *)
- "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12)
+ ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "=<|" 12)
fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
(* Execution, schedule and trace modules *)
--- a/src/HOLCF/ex/Stream.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOLCF/ex/Stream.thy Thu Apr 26 14:24:08 2007 +0200
@@ -9,7 +9,7 @@
imports HOLCF Nat_Infinity
begin
-domain 'a stream = "&&" (ft::'a) (lazy rt::"'a stream") (infixr 65)
+domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
definition
smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
--- a/src/ZF/IMP/Com.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/IMP/Com.thy Thu Apr 26 14:24:08 2007 +0200
@@ -45,8 +45,8 @@
| false
| ROp ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
| noti ("b \<in> bexp")
- | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
- | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
+ | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl "andi" 60)
+ | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl "ori" 60)
consts evalb :: i
--- a/src/ZF/Ordinal.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/Ordinal.thy Thu Apr 26 14:24:08 2007 +0200
@@ -26,16 +26,15 @@
Limit :: "i=>o"
"Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
-syntax
- "le" :: "[i,i] => o" (infixl 50) (*less-than or equals*)
+abbreviation
+ le (infixl "le" 50) where
+ "x le y == x < succ(y)"
-translations
- "x le y" == "x < succ(y)"
+notation (xsymbols)
+ le (infixl "\<le>" 50)
-syntax (xsymbols)
- "op le" :: "[i,i] => o" (infixl "\<le>" 50) (*less-than or equals*)
-syntax (HTML output)
- "op le" :: "[i,i] => o" (infixl "\<le>" 50) (*less-than or equals*)
+notation (HTML output)
+ le (infixl "\<le>" 50)
subsection{*Rules for Transset*}
--- a/src/ZF/QPair.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/QPair.thy Thu Apr 26 14:24:08 2007 +0200
@@ -41,12 +41,13 @@
"QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
syntax
- "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
- "<*>" :: "[i, i] => i" (infixr 80)
-
+ "_QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
translations
"QSUM x:A. B" => "QSigma(A, %x. B)"
- "A <*> B" => "QSigma(A, %_. B)"
+
+abbreviation
+ qprod (infixr "<*>" 80) where
+ "A <*> B == QSigma(A, %_. B)"
constdefs
qsum :: "[i,i]=>i" (infixr "<+>" 65)
@@ -62,9 +63,6 @@
"qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))"
-print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
-
-
subsection{*Quine ordered pairing*}
(** Lemmas for showing that <a;b> uniquely determines a and b **)
@@ -386,4 +384,3 @@
*}
end
-
--- a/src/ZF/Resid/Confluence.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/Resid/Confluence.thy Thu Apr 26 14:24:08 2007 +0200
@@ -66,13 +66,15 @@
consts
Sconv1 :: "i"
- "<-1->" :: "[i,i]=>o" (infixl 50)
Sconv :: "i"
- "<--->" :: "[i,i]=>o" (infixl 50)
-translations
- "a<-1->b" == "<a,b> \<in> Sconv1"
- "a<--->b" == "<a,b> \<in> Sconv"
+abbreviation
+ Sconv1_rel (infixl "<-1->" 50) where
+ "a<-1->b == <a,b> \<in> Sconv1"
+
+abbreviation
+ Sconv_rel (infixl "<--->" 50) where
+ "a<--->b == <a,b> \<in> Sconv"
inductive
domains "Sconv1" <= "lambda*lambda"
--- a/src/ZF/Resid/Redex.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/Resid/Redex.thy Thu Apr 26 14:24:08 2007 +0200
@@ -19,21 +19,19 @@
Ssub :: "i"
Scomp :: "i"
Sreg :: "i"
- union_aux :: "i=>i"
- regular :: "i=>o"
-
-(*syntax??*)
- un :: "[i,i]=>i" (infixl 70)
- "<==" :: "[i,i]=>o" (infixl 70)
- "~" :: "[i,i]=>o" (infixl 70)
+
+abbreviation
+ Ssub_rel (infixl "<==" 70) where
+ "a<==b == <a,b> \<in> Ssub"
+abbreviation
+ Scomp_rel (infixl "~" 70) where
+ "a ~ b == <a,b> \<in> Scomp"
-translations
- "a<==b" == "<a,b> \<in> Ssub"
- "a ~ b" == "<a,b> \<in> Scomp"
- "regular(a)" == "a \<in> Sreg"
+abbreviation
+ "regular(a) == a \<in> Sreg"
-
+consts union_aux :: "i=>i"
primrec (*explicit lambda is required because both arguments of "un" vary*)
"union_aux(Var(n)) =
(\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
@@ -47,13 +45,15 @@
redexes_case(%j. 0, %y. 0,
%c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
-defs
- union_def: "u un v == union_aux(u)`v"
+definition
+ union (infixl "un" 70) where
+ "u un v == union_aux(u)`v"
-syntax (xsymbols)
- "op un" :: "[i,i]=>i" (infixl "\<squnion>" 70)
- "op <==" :: "[i,i]=>o" (infixl "\<Longleftarrow>" 70)
- "op ~" :: "[i,i]=>o" (infixl "\<sim>" 70)
+notation (xsymbols)
+ union (infixl "\<squnion>" 70) and
+ Ssub_rel (infixl "\<Longleftarrow>" 70) and
+ Scomp_rel (infixl "\<sim>" 70)
+
inductive
domains "Ssub" <= "redexes*redexes"
--- a/src/ZF/Resid/Reduction.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/Resid/Reduction.thy Thu Apr 26 14:24:08 2007 +0200
@@ -74,16 +74,22 @@
Sred :: "i"
Spar_red1 :: "i"
Spar_red :: "i"
- "-1->" :: "[i,i]=>o" (infixl 50)
- "--->" :: "[i,i]=>o" (infixl 50)
- "=1=>" :: "[i,i]=>o" (infixl 50)
- "===>" :: "[i,i]=>o" (infixl 50)
+
+abbreviation
+ Sred1_rel (infixl "-1->" 50) where
+ "a -1-> b == <a,b> \<in> Sred1"
-translations
- "a -1-> b" == "<a,b> \<in> Sred1"
- "a ---> b" == "<a,b> \<in> Sred"
- "a =1=> b" == "<a,b> \<in> Spar_red1"
- "a ===> b" == "<a,b> \<in> Spar_red"
+abbreviation
+ Sred_rel (infixl "--->" 50) where
+ "a ---> b == <a,b> \<in> Sred"
+
+abbreviation
+ Spar_red1_rel (infixl "=1=>" 50) where
+ "a =1=> b == <a,b> \<in> Spar_red1"
+
+abbreviation
+ Spar_red_rel (infixl "===>" 50) where
+ "a ===> b == <a,b> \<in> Spar_red"
inductive
--- a/src/ZF/Resid/Residuals.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/Resid/Residuals.thy Thu Apr 26 14:24:08 2007 +0200
@@ -10,11 +10,10 @@
consts
Sres :: "i"
- residuals :: "[i,i,i]=>i"
- "|>" :: "[i,i]=>i" (infixl 70)
+ res_func :: "[i,i]=>i" (infixl "|>" 70)
-translations
- "residuals(u,v,w)" == "<u,v,w> \<in> Sres"
+abbreviation
+ "residuals(u,v,w) == <u,v,w> \<in> Sres"
inductive
domains "Sres" <= "redexes*redexes*redexes"
--- a/src/ZF/Resid/Substitution.thy Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/Resid/Substitution.thy Thu Apr 26 14:24:08 2007 +0200
@@ -11,7 +11,7 @@
lift_aux :: "i=>i"
lift :: "i=>i"
subst_aux :: "i=>i"
- "'/" :: "[i,i]=>i" (infixl 70) (*subst*)
+ subst :: "[i,i]=>i" (infixl "'/" 70)
constdefs
lift_rec :: "[i,i]=> i"
@@ -269,5 +269,3 @@
by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
end
-
-