equal
deleted
inserted
replaced
16 |
16 |
17 consts |
17 consts |
18 par_beta :: "(dB \<times> dB) set" |
18 par_beta :: "(dB \<times> dB) set" |
19 |
19 |
20 abbreviation |
20 abbreviation |
21 par_beta_red :: "[dB, dB] => bool" (infixl "=>" 50) |
21 par_beta_red :: "[dB, dB] => bool" (infixl "=>" 50) where |
22 "s => t == (s, t) \<in> par_beta" |
22 "s => t == (s, t) \<in> par_beta" |
23 |
23 |
24 inductive par_beta |
24 inductive par_beta |
25 intros |
25 intros |
26 var [simp, intro!]: "Var n => Var n" |
26 var [simp, intro!]: "Var n => Var n" |