# HG changeset patch
# User berghofe
# Date 1170866128 -3600
# Node ID ea31e6ea0e2ecda6b5a0ff241b9af742f2414cba
# Parent  9f3198585c899a35e7b8cbb53d946d571f5ece65
Adapted to changes in Transitive_Closure theory.

diff -r 9f3198585c89 -r ea31e6ea0e2e src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Wed Feb 07 17:34:43 2007 +0100
+++ b/src/HOL/IMP/Machines.thy	Wed Feb 07 17:35:28 2007 +0100
@@ -4,7 +4,7 @@
 theory Machines imports Natural begin
 
 lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
-  by (fast intro: rtrancl.intros elim: rtranclE)
+  by (fast intro: rtrancl_into_rtrancl elim: rtranclE)
 
 lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
   by (subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
diff -r 9f3198585c89 -r ea31e6ea0e2e src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Wed Feb 07 17:34:43 2007 +0100
+++ b/src/HOL/IMP/Transition.thy	Wed Feb 07 17:35:28 2007 +0100
@@ -200,7 +200,7 @@
   by (auto elim: evalc1.elims)
 
 lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>"
-  by (induct set: rtrancl) auto
+  by (induct set: rtrancl_set) auto
 
 (*<*)
 (* FIXME: relpow.simps don't work *)
diff -r 9f3198585c89 -r ea31e6ea0e2e src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Wed Feb 07 17:34:43 2007 +0100
+++ b/src/HOL/Induct/SList.thy	Wed Feb 07 17:35:28 2007 +0100
@@ -65,7 +65,7 @@
   
 definition
   List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" where
-  "List_rec M c d = wfrec (trancl pred_sexp)
+  "List_rec M c d = wfrec (pred_sexp^+)
                            (%g. List_case c (%x y. d x y (g y))) M"
 
 
@@ -362,7 +362,7 @@
 
 lemma List_rec_unfold_lemma:
      "(%M. List_rec M c d) == 
-      wfrec (trancl pred_sexp) (%g. List_case c (%x y. d x y (g y)))"
+      wfrec (pred_sexp^+) (%g. List_case c (%x y. d x y (g y)))"
 by (simp add: List_rec_def)
 
 lemmas List_rec_unfold =