src/HOL/Transitive_Closure.thy
changeset 14404 4952c5a92e04
parent 14398 c5c47703f763
child 14565 c6dc17aab88a
--- a/src/HOL/Transitive_Closure.thy	Fri Feb 20 14:22:51 2004 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sat Feb 21 08:43:08 2004 +0100
@@ -70,11 +70,10 @@
   thus ?thesis by rules
 qed
 
-ML_setup {*
-  bind_thm ("rtrancl_induct2", split_rule
-    (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
-*}
-
+lemmas rtrancl_induct2 =
+  rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
+                 consumes 1, case_names refl step]
+ 
 lemma trans_rtrancl: "trans(r^*)"
   -- {* transitivity of transitive closure!! -- by induction *}
 proof (rule transI)
@@ -165,7 +164,7 @@
 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
 
-theorem converse_rtrancl_induct:
+theorem converse_rtrancl_induct[consumes 1]:
   assumes major: "(a, b) : r^*"
     and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
   shows "P a"
@@ -175,10 +174,9 @@
     by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
 qed
 
-ML_setup {*
-  bind_thm ("converse_rtrancl_induct2", split_rule
-    (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));
-*}
+lemmas converse_rtrancl_induct2 =
+  converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
+                 consumes 1, case_names refl step]
 
 lemma converse_rtranclE:
   "[| (x,z):r^*;