equal
deleted
inserted
replaced
24 syntax |
24 syntax |
25 "_eta" :: "[dB, dB] => bool" (infixl "-e>" 50) |
25 "_eta" :: "[dB, dB] => bool" (infixl "-e>" 50) |
26 "_eta_rtrancl" :: "[dB, dB] => bool" (infixl "-e>>" 50) |
26 "_eta_rtrancl" :: "[dB, dB] => bool" (infixl "-e>>" 50) |
27 "_eta_reflcl" :: "[dB, dB] => bool" (infixl "-e>=" 50) |
27 "_eta_reflcl" :: "[dB, dB] => bool" (infixl "-e>=" 50) |
28 translations |
28 translations |
29 "s -e> t" == "(s,t) \<in> eta" |
29 "s -e> t" == "(s, t) \<in> eta" |
30 "s -e>> t" == "(s,t) \<in> eta^*" |
30 "s -e>> t" == "(s, t) \<in> eta^*" |
31 "s -e>= t" == "(s,t) \<in> eta^=" |
31 "s -e>= t" == "(s, t) \<in> eta^=" |
32 |
32 |
33 inductive eta |
33 inductive eta |
34 intros [simp, intro] |
34 intros [simp, intro] |
35 eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]" |
35 eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]" |
36 appL: "s -e> t ==> s $ u -e> t $ u" |
36 appL: "s -e> t ==> s $ u -e> t $ u" |