equal
deleted
inserted
replaced
15 subsection {* Parallel reduction *} |
15 subsection {* Parallel reduction *} |
16 |
16 |
17 consts |
17 consts |
18 par_beta :: "(dB \<times> dB) set" |
18 par_beta :: "(dB \<times> dB) set" |
19 |
19 |
20 syntax |
20 abbreviation (output) |
21 par_beta :: "[dB, dB] => bool" (infixl "=>" 50) |
21 par_beta_red :: "[dB, dB] => bool" (infixl "=>" 50) |
22 translations |
22 "(s => t) = ((s, t) \<in> par_beta)" |
23 "s => t" == "(s, t) \<in> par_beta" |
|
24 |
23 |
25 inductive par_beta |
24 inductive par_beta |
26 intros |
25 intros |
27 var [simp, intro!]: "Var n => Var n" |
26 var [simp, intro!]: "Var n => Var n" |
28 abs [simp, intro!]: "s => t ==> Abs s => Abs t" |
27 abs [simp, intro!]: "s => t ==> Abs s => Abs t" |