src/HOL/Lambda/WeakNorm.thy
changeset 19380 b808efaa5828
parent 19363 667b5ea637dd
child 19656 09be06943252
     1.1 --- a/src/HOL/Lambda/WeakNorm.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -366,7 +366,7 @@
     1.4    "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
     1.5  
     1.6  abbreviation (xsymbols)
     1.7 -  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
     1.8 +  rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
     1.9    "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
    1.10  
    1.11  inductive rtyping