src/HOL/W0/W0.thy
changeset 19380 b808efaa5828
parent 15236 f289e8ba2bb3
child 19736 d8d0f8f51d69
     1.1 --- a/src/HOL/W0/W0.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/W0/W0.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -382,11 +382,9 @@
     1.4  consts
     1.5    has_type :: "(typ list \<times> expr \<times> typ) set"
     1.6  
     1.7 -syntax
     1.8 -  "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
     1.9 -    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
    1.10 -translations
    1.11 -  "a |- e :: t" == "(a, e, t) \<in> has_type"
    1.12 +abbreviation
    1.13 +  has_type_rel  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
    1.14 +  "a |- e :: t == (a, e, t) \<in> has_type"
    1.15  
    1.16  inductive has_type
    1.17    intros