eliminated unnamed infixes, tuned syntax;
authorwenzelm
Thu Apr 26 14:24:08 2007 +0200 (2007-04-26)
changeset 22808a7daa74e2980
parent 22807 715d01b34abb
child 22809 3cf5df73d50a
eliminated unnamed infixes, tuned syntax;
src/CTT/CTT.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_permeq.ML
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/ex/Stream.thy
src/ZF/IMP/Com.thy
src/ZF/Ordinal.thy
src/ZF/QPair.thy
src/ZF/Resid/Confluence.thy
src/ZF/Resid/Redex.thy
src/ZF/Resid/Reduction.thy
src/ZF/Resid/Residuals.thy
src/ZF/Resid/Substitution.thy
     1.1 --- a/src/CTT/CTT.thy	Thu Apr 26 13:33:17 2007 +0200
     1.2 +++ b/src/CTT/CTT.thy	Thu Apr 26 14:24:08 2007 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    (*General Product and Function Space*)
     1.5    Prod      :: "[t, i=>t]=>t"
     1.6    (*Types*)
     1.7 -  "+"       :: "[t,t]=>t"           (infixr 40)
     1.8 +  Plus      :: "[t,t]=>t"           (infixr "+" 40)
     1.9    (*Equality type*)
    1.10    Eq        :: "[t,i,i]=>t"
    1.11    eq        :: "i"
    1.12 @@ -51,7 +51,7 @@
    1.13  
    1.14    (*Functions*)
    1.15    lambda    :: "(i => i) => i"      (binder "lam " 10)
    1.16 -  "`"       :: "[i,i]=>i"           (infixl 60)
    1.17 +  app       :: "[i,i]=>i"           (infixl "`" 60)
    1.18    (*Natural numbers*)
    1.19    "0"       :: "i"                  ("0")
    1.20    (*Pairing*)
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Thu Apr 26 13:33:17 2007 +0200
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Thu Apr 26 14:24:08 2007 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  text {* Most constants are already declared by HOL. *}
     2.5  
     2.6  consts
     2.7 -  assoc         :: "['a::times, 'a] => bool"              (infixl 50)
     2.8 +  assoc         :: "['a::times, 'a] => bool"              (infixl "assoc" 50)
     2.9    irred         :: "'a::{zero, one, times} => bool"
    2.10    prime         :: "'a::{zero, one, times} => bool"
    2.11  
     3.1 --- a/src/HOL/Hyperreal/Poly.thy	Thu Apr 26 13:33:17 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Poly.thy	Thu Apr 26 14:24:08 2007 +0200
     3.3 @@ -23,20 +23,20 @@
     3.4  subsection{*Arithmetic Operations on Polynomials*}
     3.5  
     3.6  text{*addition*}
     3.7 -consts "+++" :: "[real list, real list] => real list"  (infixl 65)
     3.8 +consts padd :: "[real list, real list] => real list"  (infixl "+++" 65)
     3.9  primrec
    3.10    padd_Nil:  "[] +++ l2 = l2"
    3.11    padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
    3.12                              else (h + hd l2)#(t +++ tl l2))"
    3.13  
    3.14  text{*Multiplication by a constant*}
    3.15 -consts "%*" :: "[real, real list] => real list"  (infixl 70)
    3.16 +consts cmult :: "[real, real list] => real list"  (infixl "%*" 70)
    3.17  primrec
    3.18     cmult_Nil:  "c %* [] = []"
    3.19     cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
    3.20  
    3.21  text{*Multiplication by a polynomial*}
    3.22 -consts "***" :: "[real list, real list] => real list"  (infixl 70)
    3.23 +consts pmult :: "[real list, real list] => real list"  (infixl "***" 70)
    3.24  primrec
    3.25     pmult_Nil:  "[] *** l2 = []"
    3.26     pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
    3.27 @@ -50,7 +50,7 @@
    3.28  
    3.29  
    3.30  text{*Exponential*}
    3.31 -consts "%^" :: "[real list, nat] => real list"  (infixl 80)
    3.32 +consts pexp :: "[real list, nat] => real list"  (infixl "%^" 80)
    3.33  primrec
    3.34     pexp_0:   "p %^ 0 = [1]"
    3.35     pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
     4.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Apr 26 13:33:17 2007 +0200
     4.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Apr 26 14:24:08 2007 +0200
     4.3 @@ -176,7 +176,7 @@
     4.4     fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80)
     4.5     "a \<sharp> x \<equiv> a \<notin> supp x"
     4.6  
     4.7 -   supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)
     4.8 +   supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80)
     4.9     "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
    4.10  
    4.11  lemma supp_fresh_iff: 
    4.12 @@ -1770,7 +1770,7 @@
    4.13    and      b: "S1 \<subseteq> S2"
    4.14    shows "S2 supports x"
    4.15    using a b
    4.16 -  by (force simp add: "op supports_def")
    4.17 +  by (force simp add: supports_def)
    4.18  
    4.19  lemma supp_is_subset:
    4.20    fixes S :: "'x set"
    4.21 @@ -1782,7 +1782,7 @@
    4.22    assume "\<not>(supp x \<subseteq> S)"
    4.23    hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
    4.24    then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
    4.25 -  from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
    4.26 +  from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold supports_def, force)
    4.27    hence "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by force
    4.28    with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
    4.29    hence "a\<notin>(supp x)" by (unfold supp_def, auto)
    4.30 @@ -1794,7 +1794,7 @@
    4.31    assumes  pt: "pt TYPE('a) TYPE('x)"
    4.32    and      at: "at TYPE ('x)"
    4.33    shows "((supp x)::'x set) supports x"
    4.34 -proof (unfold "op supports_def", intro strip)
    4.35 +proof (unfold supports_def, intro strip)
    4.36    fix a b
    4.37    assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
    4.38    hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
    4.39 @@ -1860,7 +1860,7 @@
    4.40    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)"
    4.41    shows  "S supports X"
    4.42  using a
    4.43 -apply(auto simp add: "op supports_def")
    4.44 +apply(auto simp add: supports_def)
    4.45  apply(simp add: pt_set_bij1a[OF pt, OF at])
    4.46  apply(force simp add: pt_swap_bij[OF pt, OF at])
    4.47  apply(simp add: pt_set_bij1a[OF pt, OF at])
    4.48 @@ -1885,7 +1885,7 @@
    4.49    shows "X supports X"
    4.50  proof -
    4.51    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])
    4.52 -  then show ?thesis by (simp add: "op supports_def")
    4.53 +  then show ?thesis by (simp add: supports_def)
    4.54  qed
    4.55  
    4.56  lemma infinite_Collection:
    4.57 @@ -2076,7 +2076,7 @@
    4.58    shows "supp (f x) \<subseteq> (((supp f)\<union>(supp x))::'x set)"
    4.59  proof -
    4.60    have s1: "((supp f)\<union>((supp x)::'x set)) supports (f x)"
    4.61 -  proof (simp add: "op supports_def", fold fresh_def, auto)
    4.62 +  proof (simp add: supports_def, fold fresh_def, auto)
    4.63      fix a::"'x" and b::"'x"
    4.64      assume "a\<sharp>f" and "b\<sharp>f"
    4.65      hence a1: "[(a,b)]\<bullet>f = f" 
    4.66 @@ -2171,7 +2171,7 @@
    4.67    assumes pt: "pt TYPE('a) TYPE('x)"
    4.68    and     at: "at TYPE('x)"
    4.69    shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
    4.70 -  apply(simp add: "op supports_def" fresh_def[symmetric])
    4.71 +  apply(simp add: supports_def fresh_def[symmetric])
    4.72    apply(rule allI)+
    4.73    apply(rule impI)
    4.74    apply(erule conjE)
    4.75 @@ -2592,7 +2592,7 @@
    4.76    and     f1: "finite ((supp h)::'x set)"
    4.77    and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
    4.78    shows "((supp h)::'x set) supports (fresh_fun h)"
    4.79 -  apply(simp add: "op supports_def" fresh_def[symmetric])
    4.80 +  apply(simp add: supports_def fresh_def[symmetric])
    4.81    apply(auto)
    4.82    apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a])
    4.83    apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
     5.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 26 13:33:17 2007 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 26 14:24:08 2007 +0200
     5.3 @@ -55,7 +55,7 @@
     5.4  val not_false     = thm "not_False_eq_True"
     5.5  val perm_fun_def  = thm "Nominal.perm_fun_def"
     5.6  val perm_eq_app   = thm "Nominal.pt_fun_app_eq"
     5.7 -val supports_def  = thm "Nominal.op supports_def";
     5.8 +val supports_def  = thm "Nominal.supports_def";
     5.9  val fresh_def     = thm "Nominal.fresh_def";
    5.10  val fresh_prod    = thm "Nominal.fresh_prod";
    5.11  val fresh_unit    = thm "Nominal.fresh_unit";
     6.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Apr 26 13:33:17 2007 +0200
     6.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Apr 26 14:24:08 2007 +0200
     6.3 @@ -57,7 +57,7 @@
     6.4    (* binary composition of action signatures and automata *)
     6.5    asig_comp    ::"['a signature, 'a signature] => 'a signature"
     6.6    compatible   ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
     6.7 -  "||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr 10)
     6.8 +  par          ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
     6.9  
    6.10    (* hiding and restricting *)
    6.11    hide_asig     :: "['a signature, 'a set] => 'a signature"
    6.12 @@ -86,7 +86,9 @@
    6.13  
    6.14    "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"
    6.15                    ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
    6.16 -  "op ||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "\<parallel>" 10)
    6.17 +
    6.18 +notation (xsymbols)
    6.19 +  par  (infixr "\<parallel>" 10)
    6.20  
    6.21  
    6.22  inductive "reachable C"
     7.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Apr 26 13:33:17 2007 +0200
     7.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Apr 26 14:24:08 2007 +0200
     7.3 @@ -9,7 +9,7 @@
     7.4  imports HOLCF
     7.5  begin
     7.6  
     7.7 -domain 'a seq = nil | "##" (HD :: 'a) (lazy TL :: "'a seq")  (infixr 65)
     7.8 +domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
     7.9  
    7.10  consts
    7.11     sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
    7.12 @@ -30,14 +30,13 @@
    7.13     nproj        :: "nat => 'a seq => 'a"
    7.14     sproj        :: "nat => 'a seq => 'a seq"
    7.15  
    7.16 -syntax
    7.17 -   "@@"         :: "'a seq => 'a seq => 'a seq" (infixr 65)
    7.18 -   "Finite"     :: "'a seq => bool"
    7.19 +abbreviation
    7.20 +  sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
    7.21 +  "xs @@ ys == sconc $ xs $ ys"
    7.22  
    7.23 -translations
    7.24 -   "xs @@ ys" == "sconc $ xs $ ys"
    7.25 -   "Finite x" == "x:sfinite"
    7.26 -   "~(Finite x)" =="x~:sfinite"
    7.27 +abbreviation
    7.28 +  Finite :: "'a seq => bool" where
    7.29 +  "Finite x == x:sfinite"
    7.30  
    7.31  defs
    7.32  
     8.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Apr 26 13:33:17 2007 +0200
     8.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Apr 26 14:24:08 2007 +0200
     8.3 @@ -58,7 +58,7 @@
     8.4    fairtraces     ::"('a,'s)ioa => 'a trace set"
     8.5  
     8.6    (* Notions of implementation *)
     8.7 -  "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr 12)
     8.8 +  ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr "=<|" 12)
     8.9    fair_implements  :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
    8.10  
    8.11    (* Execution, schedule and trace modules *)
     9.1 --- a/src/HOLCF/ex/Stream.thy	Thu Apr 26 13:33:17 2007 +0200
     9.2 +++ b/src/HOLCF/ex/Stream.thy	Thu Apr 26 14:24:08 2007 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4  imports HOLCF Nat_Infinity
     9.5  begin
     9.6  
     9.7 -domain 'a stream = "&&" (ft::'a) (lazy rt::"'a stream") (infixr 65)
     9.8 +domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
     9.9  
    9.10  definition
    9.11    smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
    10.1 --- a/src/ZF/IMP/Com.thy	Thu Apr 26 13:33:17 2007 +0200
    10.2 +++ b/src/ZF/IMP/Com.thy	Thu Apr 26 14:24:08 2007 +0200
    10.3 @@ -45,8 +45,8 @@
    10.4         | false
    10.5         | ROp  ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
    10.6         | noti ("b \<in> bexp")
    10.7 -       | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
    10.8 -       | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
    10.9 +       | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl "andi" 60)
   10.10 +       | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl "ori" 60)
   10.11  
   10.12  
   10.13  consts evalb :: i
    11.1 --- a/src/ZF/Ordinal.thy	Thu Apr 26 13:33:17 2007 +0200
    11.2 +++ b/src/ZF/Ordinal.thy	Thu Apr 26 14:24:08 2007 +0200
    11.3 @@ -26,16 +26,15 @@
    11.4    Limit         :: "i=>o"
    11.5      "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
    11.6  
    11.7 -syntax
    11.8 -  "le"          :: "[i,i] => o"  (infixl 50)   (*less-than or equals*)
    11.9 +abbreviation
   11.10 +  le  (infixl "le" 50) where
   11.11 +  "x le y == x < succ(y)"
   11.12  
   11.13 -translations
   11.14 -  "x le y"      == "x < succ(y)"
   11.15 +notation (xsymbols)
   11.16 +  le  (infixl "\<le>" 50)
   11.17  
   11.18 -syntax (xsymbols)
   11.19 -  "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
   11.20 -syntax (HTML output)
   11.21 -  "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
   11.22 +notation (HTML output)
   11.23 +  le  (infixl "\<le>" 50)
   11.24  
   11.25  
   11.26  subsection{*Rules for Transset*}
    12.1 --- a/src/ZF/QPair.thy	Thu Apr 26 13:33:17 2007 +0200
    12.2 +++ b/src/ZF/QPair.thy	Thu Apr 26 14:24:08 2007 +0200
    12.3 @@ -41,12 +41,13 @@
    12.4      "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
    12.5  
    12.6  syntax
    12.7 -  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
    12.8 -  "<*>"     :: "[i, i] => i"                      (infixr 80)
    12.9 -
   12.10 +  "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
   12.11  translations
   12.12    "QSUM x:A. B"  => "QSigma(A, %x. B)"
   12.13 -  "A <*> B"      => "QSigma(A, %_. B)"
   12.14 +
   12.15 +abbreviation
   12.16 +  qprod  (infixr "<*>" 80) where
   12.17 +  "A <*> B == QSigma(A, %_. B)"
   12.18  
   12.19  constdefs
   12.20    qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)
   12.21 @@ -62,9 +63,6 @@
   12.22      "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
   12.23  
   12.24  
   12.25 -print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
   12.26 -
   12.27 -
   12.28  subsection{*Quine ordered pairing*}
   12.29  
   12.30  (** Lemmas for showing that <a;b> uniquely determines a and b **)
   12.31 @@ -386,4 +384,3 @@
   12.32  *}
   12.33  
   12.34  end
   12.35 -
    13.1 --- a/src/ZF/Resid/Confluence.thy	Thu Apr 26 13:33:17 2007 +0200
    13.2 +++ b/src/ZF/Resid/Confluence.thy	Thu Apr 26 14:24:08 2007 +0200
    13.3 @@ -66,13 +66,15 @@
    13.4  
    13.5  consts
    13.6    Sconv1        :: "i"
    13.7 -  "<-1->"       :: "[i,i]=>o"   (infixl 50)
    13.8    Sconv         :: "i"
    13.9 -  "<--->"       :: "[i,i]=>o"   (infixl 50)
   13.10  
   13.11 -translations
   13.12 -  "a<-1->b"    == "<a,b> \<in> Sconv1"
   13.13 -  "a<--->b"    == "<a,b> \<in> Sconv"
   13.14 +abbreviation
   13.15 +  Sconv1_rel (infixl "<-1->" 50) where
   13.16 +  "a<-1->b == <a,b> \<in> Sconv1"
   13.17 +
   13.18 +abbreviation
   13.19 +  Sconv_rel (infixl "<--->" 50) where
   13.20 +  "a<--->b == <a,b> \<in> Sconv"
   13.21    
   13.22  inductive
   13.23    domains       "Sconv1" <= "lambda*lambda"
    14.1 --- a/src/ZF/Resid/Redex.thy	Thu Apr 26 13:33:17 2007 +0200
    14.2 +++ b/src/ZF/Resid/Redex.thy	Thu Apr 26 14:24:08 2007 +0200
    14.3 @@ -19,21 +19,19 @@
    14.4    Ssub  :: "i"
    14.5    Scomp :: "i"
    14.6    Sreg  :: "i"
    14.7 -  union_aux        :: "i=>i"
    14.8 -  regular          :: "i=>o"
    14.9 -  
   14.10 -(*syntax??*)
   14.11 -  un               :: "[i,i]=>i"  (infixl 70)
   14.12 -  "<=="            :: "[i,i]=>o"  (infixl 70)
   14.13 -  "~"              :: "[i,i]=>o"  (infixl 70)
   14.14 +
   14.15 +abbreviation
   14.16 +  Ssub_rel  (infixl "<==" 70) where
   14.17 +  "a<==b == <a,b> \<in> Ssub"
   14.18  
   14.19 +abbreviation
   14.20 +  Scomp_rel  (infixl "~" 70) where
   14.21 +  "a ~ b == <a,b> \<in> Scomp"
   14.22  
   14.23 -translations
   14.24 -  "a<==b"        == "<a,b> \<in> Ssub"
   14.25 -  "a ~ b"        == "<a,b> \<in> Scomp"
   14.26 -  "regular(a)"   == "a \<in> Sreg"
   14.27 +abbreviation
   14.28 +  "regular(a) == a \<in> Sreg"
   14.29  
   14.30 -
   14.31 +consts union_aux        :: "i=>i"
   14.32  primrec (*explicit lambda is required because both arguments of "un" vary*)
   14.33    "union_aux(Var(n)) =
   14.34       (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
   14.35 @@ -47,13 +45,15 @@
   14.36          redexes_case(%j. 0, %y. 0,
   14.37  		     %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
   14.38  
   14.39 -defs
   14.40 -  union_def:  "u un v == union_aux(u)`v"
   14.41 +definition
   14.42 +  union  (infixl "un" 70) where
   14.43 +  "u un v == union_aux(u)`v"
   14.44  
   14.45 -syntax (xsymbols)
   14.46 -  "op un"             :: "[i,i]=>i"  (infixl "\<squnion>" 70)
   14.47 -  "op <=="            :: "[i,i]=>o"  (infixl "\<Longleftarrow>" 70)
   14.48 -  "op ~"              :: "[i,i]=>o"  (infixl "\<sim>" 70)
   14.49 +notation (xsymbols)
   14.50 +  union  (infixl "\<squnion>" 70) and
   14.51 +  Ssub_rel  (infixl "\<Longleftarrow>" 70) and
   14.52 +  Scomp_rel  (infixl "\<sim>" 70)
   14.53 +
   14.54  
   14.55  inductive
   14.56    domains       "Ssub" <= "redexes*redexes"
    15.1 --- a/src/ZF/Resid/Reduction.thy	Thu Apr 26 13:33:17 2007 +0200
    15.2 +++ b/src/ZF/Resid/Reduction.thy	Thu Apr 26 14:24:08 2007 +0200
    15.3 @@ -74,16 +74,22 @@
    15.4    Sred      :: "i"
    15.5    Spar_red1 :: "i"
    15.6    Spar_red  :: "i"
    15.7 -  "-1->"    :: "[i,i]=>o"  (infixl 50)
    15.8 -  "--->"    :: "[i,i]=>o"  (infixl 50)
    15.9 -  "=1=>"    :: "[i,i]=>o"  (infixl 50)
   15.10 -  "===>"    :: "[i,i]=>o"  (infixl 50)
   15.11 +
   15.12 +abbreviation
   15.13 +  Sred1_rel (infixl "-1->" 50) where
   15.14 +  "a -1-> b == <a,b> \<in> Sred1"
   15.15  
   15.16 -translations
   15.17 -  "a -1-> b" == "<a,b> \<in> Sred1"
   15.18 -  "a ---> b" == "<a,b> \<in> Sred"
   15.19 -  "a =1=> b" == "<a,b> \<in> Spar_red1"
   15.20 -  "a ===> b" == "<a,b> \<in> Spar_red"
   15.21 +abbreviation
   15.22 +  Sred_rel (infixl "--->" 50) where
   15.23 +  "a ---> b == <a,b> \<in> Sred"
   15.24 +
   15.25 +abbreviation
   15.26 +  Spar_red1_rel (infixl "=1=>" 50) where
   15.27 +  "a =1=> b == <a,b> \<in> Spar_red1"
   15.28 +
   15.29 +abbreviation
   15.30 +  Spar_red_rel (infixl "===>" 50) where
   15.31 +  "a ===> b == <a,b> \<in> Spar_red"
   15.32    
   15.33    
   15.34  inductive
    16.1 --- a/src/ZF/Resid/Residuals.thy	Thu Apr 26 13:33:17 2007 +0200
    16.2 +++ b/src/ZF/Resid/Residuals.thy	Thu Apr 26 14:24:08 2007 +0200
    16.3 @@ -10,11 +10,10 @@
    16.4  
    16.5  consts
    16.6    Sres          :: "i"
    16.7 -  residuals     :: "[i,i,i]=>i"
    16.8 -  "|>"          :: "[i,i]=>i"     (infixl 70)
    16.9 +  res_func      :: "[i,i]=>i"     (infixl "|>" 70)
   16.10  
   16.11 -translations
   16.12 -  "residuals(u,v,w)"  == "<u,v,w> \<in> Sres"
   16.13 +abbreviation
   16.14 +  "residuals(u,v,w) == <u,v,w> \<in> Sres"
   16.15  
   16.16  inductive
   16.17    domains       "Sres" <= "redexes*redexes*redexes"
    17.1 --- a/src/ZF/Resid/Substitution.thy	Thu Apr 26 13:33:17 2007 +0200
    17.2 +++ b/src/ZF/Resid/Substitution.thy	Thu Apr 26 14:24:08 2007 +0200
    17.3 @@ -11,7 +11,7 @@
    17.4    lift_aux      :: "i=>i"
    17.5    lift          :: "i=>i"
    17.6    subst_aux     :: "i=>i"
    17.7 -  "'/"          :: "[i,i]=>i"  (infixl 70)  (*subst*)
    17.8 +  subst         :: "[i,i]=>i"  (infixl "'/" 70)
    17.9  
   17.10  constdefs
   17.11    lift_rec      :: "[i,i]=> i"
   17.12 @@ -269,5 +269,3 @@
   17.13  by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
   17.14  
   17.15  end
   17.16 -
   17.17 -