src/HOL/Lambda/Lambda.thy
changeset 9827 ce6e22ff89c3
parent 9811 39ffdb8cab03
child 9906 5c027cca6262
equal deleted inserted replaced
9826:5b5d9ee742ca 9827:ce6e22ff89c3
    58 
    58 
    59 syntax
    59 syntax
    60   "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
    60   "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
    61   "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
    61   "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
    62 translations
    62 translations
    63   "s -> t" == "(s,t) \<in> beta"
    63   "s -> t" == "(s, t) \<in> beta"
    64   "s ->> t" == "(s,t) \<in> beta^*"
    64   "s ->> t" == "(s, t) \<in> beta^*"
    65 
    65 
    66 inductive beta
    66 inductive beta
    67   intros [simp, intro!]
    67   intros [simp, intro!]
    68     beta: "Abs s $ t -> s[t/0]"
    68     beta: "Abs s $ t -> s[t/0]"
    69     appL: "s -> t ==> s $ u -> t $ u"
    69     appL: "s -> t ==> s $ u -> t $ u"