# HG changeset patch
# User wenzelm
# Date 1177590248 -7200
# Node ID a7daa74e29805a290c0ceb3db4b0d905c4f3fd0f
# Parent  715d01b34abbbdee4683dd5cfc5158091df0997f
eliminated unnamed infixes, tuned syntax;

diff -r 715d01b34abb -r a7daa74e2980 src/CTT/CTT.thy
--- 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*)
diff -r 715d01b34abb -r a7daa74e2980 src/HOL/Algebra/abstract/Ring2.thy
--- 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"
 
diff -r 715d01b34abb -r a7daa74e2980 src/HOL/Hyperreal/Poly.thy
--- 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)"
diff -r 715d01b34abb -r a7daa74e2980 src/HOL/Nominal/Nominal.thy
--- 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])
diff -r 715d01b34abb -r a7daa74e2980 src/HOL/Nominal/nominal_permeq.ML
--- 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";
diff -r 715d01b34abb -r a7daa74e2980 src/HOLCF/IOA/meta_theory/Automata.thy
--- 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"
diff -r 715d01b34abb -r a7daa74e2980 src/HOLCF/IOA/meta_theory/Seq.thy
--- 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
 
diff -r 715d01b34abb -r a7daa74e2980 src/HOLCF/IOA/meta_theory/Traces.thy
--- 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 *)
diff -r 715d01b34abb -r a7daa74e2980 src/HOLCF/ex/Stream.thy
--- 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
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/IMP/Com.thy
--- 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
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/Ordinal.thy
--- 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*}
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/QPair.thy
--- 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
-
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/Resid/Confluence.thy
--- 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"
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/Resid/Redex.thy
--- 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"
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/Resid/Reduction.thy
--- 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
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/Resid/Residuals.thy
--- 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"
diff -r 715d01b34abb -r a7daa74e2980 src/ZF/Resid/Substitution.thy
--- 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
-
-