1.1 --- a/src/HOL/Lambda/Type.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Lambda/Type.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -16,6 +16,8 @@
     1.4    "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
     1.5  syntax (xsymbols)
     1.6    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
     1.7 +syntax (HTML output)
     1.8 +  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
     1.9  
    1.10  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
    1.11    by (simp add: shift_def)