equal
deleted
inserted
replaced
381 |
381 |
382 fun dblam_in where |
382 fun dblam_in where |
383 "dblam_in None = None" |
383 "dblam_in None = None" |
384 | "dblam_in (Some x) = Some (DBLam x)" |
384 | "dblam_in (Some x) = Some (DBLam x)" |
385 |
385 |
386 lemma [eqvt]: |
386 lemma db_in_eqvt[eqvt]: |
387 "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)" |
387 "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)" |
388 "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)" |
388 "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)" |
389 apply (case_tac [!] x) |
389 apply (case_tac [!] x) |
390 apply (simp_all add: eqvts) |
390 apply (simp_all add: eqvts) |
391 apply (case_tac y) |
391 apply (case_tac y) |