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.9  
    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.18  
    1.19  
    1.20  subsection {* Coiteration (unfold) *}