# HG changeset patch
# User blanchet
# Date 1348404773 -7200
# Node ID 69ee9f96c423fcea886785a365da3bd6293d7ed8
# Parent  8bb6e2d7346be5b7e684959fbf3462c7bf2a9a25
adapted examples to new names

diff -r 8bb6e2d7346b -r 69ee9f96c423 src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Sun Sep 23 14:52:53 2012 +0200
@@ -130,7 +130,7 @@
           \<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow>
           n1 = n2 \<and> llift2 \<phi> as1 as2"
 shows "tr1 = tr2"
-apply(rule mp[OF Tree.rel_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
+apply(rule mp[OF Tree.dtor_rel_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
   fix tr1 tr2  assume \<phi>: "\<phi> tr1 tr2"
   show "pre_Tree_rel \<phi> (Tree_dtor tr1) (Tree_dtor tr2)"
   apply(cases rule: Tree.ctor_exhaust[of tr1], cases rule: Tree.ctor_exhaust[of tr2])
diff -r 8bb6e2d7346b -r 69ee9f96c423 src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Sun Sep 23 14:52:53 2012 +0200
@@ -45,7 +45,7 @@
 Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
 Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
 shows "p = p'"
-proof(intro mp[OF process.rel_coinduct, of \<phi>, OF _ phi], clarify)
+proof(intro mp[OF process.dtor_rel_coinduct, of \<phi>, OF _ phi], clarify)
   fix p p'  assume \<phi>: "\<phi> p p'"
   show "pre_process_rel (op =) \<phi> (process_dtor p) (process_dtor p')"
   proof(cases rule: process.exhaust[of p])
@@ -75,7 +75,7 @@
 Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> (\<phi> p p' \<or> p = p')" and
 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')"
 shows "p = p'"
-proof(intro mp[OF process.rel_strong_coinduct, of \<phi>, OF _ phi], clarify)
+proof(intro mp[OF process.dtor_rel_strong_coinduct, of \<phi>, OF _ phi], clarify)
   fix p p'  assume \<phi>: "\<phi> p p'"
   show "pre_process_rel (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_dtor p) (process_dtor p')"
   proof(cases rule: process.exhaust[of p])
diff -r 8bb6e2d7346b -r 69ee9f96c423 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Sun Sep 23 14:52:53 2012 +0200
@@ -122,7 +122,7 @@
 unfolding prod_rel_def by auto
 
 lemmas stream_coind =
-  mp[OF stream.rel_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def]
+  mp[OF stream.dtor_rel_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def]
 
 definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
   [simp]: "plus xs ys =
diff -r 8bb6e2d7346b -r 69ee9f96c423 src/HOL/BNF/Examples/TreeFsetI.thy
--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Sun Sep 23 14:52:53 2012 +0200
@@ -50,7 +50,7 @@
 apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def)
 done
 
-lemmas treeFsetI_coind = mp[OF treeFsetI.rel_coinduct]
+lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_rel_coinduct]
 
 lemma "tmap (f o g) x = tmap f (tmap g x)"
 by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])