--- a/src/HOL/Lambda/WeakNorm.thy Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Sun Apr 09 18:51:13 2006 +0200
@@ -366,7 +366,7 @@
"e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
abbreviation (xsymbols)
- rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
+ rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
"e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
inductive rtyping