--- a/src/HOL/W0/W0.thy Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/W0/W0.thy Sun Apr 09 18:51:13 2006 +0200
@@ -382,11 +382,9 @@
consts
has_type :: "(typ list \<times> expr \<times> typ) set"
-syntax
- "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
- ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
-translations
- "a |- e :: t" == "(a, e, t) \<in> has_type"
+abbreviation
+ has_type_rel ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
+ "a |- e :: t == (a, e, t) \<in> has_type"
inductive has_type
intros