src/HOL/BNF_Examples/Process.thy
 changeset 57983 6edc3529bb4e parent 55944 7ab8f003fe41 child 58249 180f1b3508ed
1.1 --- a/src/HOL/BNF_Examples/Process.thy	Mon Aug 18 15:03:25 2014 +0200
1.2 +++ b/src/HOL/BNF_Examples/Process.thy	Mon Aug 18 17:19:58 2014 +0200
1.3 @@ -29,7 +29,7 @@
1.4  (* Constructors versus discriminators *)
1.5  theorem isAction_isChoice:
1.6  "isAction p \<or> isChoice p"
1.7 -by (rule process.disc_exhaust) auto
1.8 +by (rule process.exhaust_disc) auto
1.10  theorem not_isAction_isChoice: "\<not> (isAction p \<and> isChoice p)"
1.11  by (cases rule: process.exhaust[of p]) auto
1.12 @@ -54,7 +54,7 @@
1.13    Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
1.14    shows "p = p'"
1.15    using assms
1.16 -  by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.disc(3))
1.17 +  by (coinduct rule: process.coinduct_strong) (metis process.collapse(1,2) process.disc(3))
1.20  subsection {* Coiteration (unfold) *}