src/HOL/Lambda/WeakNorm.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 19380 b808efaa5828
     1.1 --- a/src/HOL/Lambda/WeakNorm.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -361,11 +361,13 @@
     1.4  consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
     1.5    rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
    1.10 -  "(e |-\<^sub>R t : T) = ((e, t, T) \<in> rtyping)"
    1.11 -syntax (xsymbols)
    1.12 +  "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
    1.13 +
    1.14 +abbreviation (xsymbols)
    1.15    rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
    1.16 +  "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
    1.17  
    1.18  inductive rtyping
    1.19    intros