equal
deleted
inserted
replaced
55 |
55 |
56 consts |
56 consts |
57 beta :: "(dB \<times> dB) set" |
57 beta :: "(dB \<times> dB) set" |
58 |
58 |
59 abbreviation |
59 abbreviation |
60 beta_red :: "[dB, dB] => bool" (infixl "->" 50) |
60 beta_red :: "[dB, dB] => bool" (infixl "->" 50) where |
61 "s -> t == (s, t) \<in> beta" |
61 "s -> t == (s, t) \<in> beta" |
62 beta_reds :: "[dB, dB] => bool" (infixl "->>" 50) |
62 |
|
63 abbreviation |
|
64 beta_reds :: "[dB, dB] => bool" (infixl "->>" 50) where |
63 "s ->> t == (s, t) \<in> beta^*" |
65 "s ->> t == (s, t) \<in> beta^*" |
64 |
66 |
65 notation (latex) |
67 notation (latex) |
66 beta_red (infixl "\<rightarrow>\<^sub>\<beta>" 50) |
68 beta_red (infixl "\<rightarrow>\<^sub>\<beta>" 50) and |
67 beta_reds (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) |
69 beta_reds (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) |
68 |
70 |
69 inductive beta |
71 inductive beta |
70 intros |
72 intros |
71 beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" |
73 beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" |