src/HOL/Lambda/Type.thy
changeset 19380 b808efaa5828
parent 19363 667b5ea637dd
child 19656 09be06943252
     1.1 --- a/src/HOL/Lambda/Type.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Type.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -16,12 +16,12 @@
     1.4    "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
     1.5  
     1.6  abbreviation (xsymbols)
     1.7 -  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
     1.8 +  shift1  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
     1.9    "e\<langle>i:a\<rangle> == e<i:a>"
    1.10  
    1.11  abbreviation (HTML output)
    1.12 -  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    1.13 -  "shift == xsymbols.shift"
    1.14 +  shift2  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    1.15 +  "shift2 == shift"
    1.16  
    1.17  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
    1.18    by (simp add: shift_def)
    1.19 @@ -63,13 +63,13 @@
    1.20    "env ||- ts : Ts == typings env ts Ts"
    1.21  
    1.22  abbreviation (xsymbols)
    1.23 -  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    1.24 +  typing_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    1.25    "env \<turnstile> t : T == env |- t : T"
    1.26  
    1.27  abbreviation (latex)
    1.28 -  funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
    1.29 +  funs2 :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
    1.30    "op \<Rrightarrow> == op =>>"
    1.31 -  typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    1.32 +  typings_rel2 :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    1.33      ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    1.34    "env \<tturnstile> ts : Ts == env ||- ts : Ts"
    1.35