src/HOL/Isar_examples/W_correct.thy
changeset 11628 e57a6e51715e
parent 10408 d8b3613158b1
child 11809 c9ffdd63dd93
equal deleted inserted replaced
11627:abf9cda4a4d2 11628:e57a6e51715e
    31     ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
    31     ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
    32 translations
    32 translations
    33   "a |- e :: t" == "(a, e, t) : has_type"
    33   "a |- e :: t" == "(a, e, t) : has_type"
    34 
    34 
    35 inductive has_type
    35 inductive has_type
    36   intros [simp]
    36   intros
    37     Var: "n < length a ==> a |- Var n :: a ! n"
    37     Var [simp]: "n < length a ==> a |- Var n :: a ! n"
    38     Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    38     Abs [simp]: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    39     App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
    39     App [simp]: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
    40       ==> a |- App e1 e2 :: t1"
    40       ==> a |- App e1 e2 :: t1"
    41 
    41 
    42 
    42 
    43 text {* Type assigment is closed wrt.\ substitution. *}
    43 text {* Type assigment is closed wrt.\ substitution. *}
    44 
    44