# HG changeset patch
# User nipkow
# Date 971113798 -7200
# Node ID 9d5678e6bf343a797dad36c7f1916c05be23df47
# Parent  aecb5bf6f76f1d5e21a7ec2e744b02c21c7b4827
added rtranclIs

diff -r aecb5bf6f76f -r 9d5678e6bf34 src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Mon Oct 09 19:20:55 2000 +0200
+++ b/src/HOL/Induct/Comb.ML	Mon Oct 09 19:49:58 2000 +0200
@@ -65,12 +65,12 @@
 
 Goal "x ---> y ==> x#z ---> y#z";
 by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
+by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
 qed "Ap_reduce1";
 
 Goal "x ---> y ==> z#x ---> z#y";
 by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
+by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
 qed "Ap_reduce2";
 
 (** Counterexample to the diamond property for -1-> **)
diff -r aecb5bf6f76f -r 9d5678e6bf34 src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Mon Oct 09 19:20:55 2000 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Mon Oct 09 19:49:58 2000 +0200
@@ -132,7 +132,7 @@
        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
   apply (erule rtrancl_induct)
    apply blast
-  apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)
+  apply (blast del: rtrancl_refl intro: rtranclIs)
   done
 
-end
\ No newline at end of file
+end
diff -r aecb5bf6f76f -r 9d5678e6bf34 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Mon Oct 09 19:20:55 2000 +0200
+++ b/src/HOL/Trancl.ML	Mon Oct 09 19:49:58 2000 +0200
@@ -97,7 +97,7 @@
 qed "rtranclE";
 
 bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
-
+bind_thms("rtranclIs", [r_into_rtrancl, rtrancl_trans]);
 
 (*** More r^* equations and inclusions ***)
 
@@ -106,14 +106,14 @@
 by (etac r_into_rtrancl 2);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+by (blast_tac (claset() addIs rtranclIs) 1);
 qed "rtrancl_idemp";
 Addsimps [rtrancl_idemp];
 
 Goal "R^* O R^* = R^*";
 by (rtac set_ext 1);
 by (split_all_tac 1);
-by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+by (blast_tac (claset() addIs rtranclIs) 1);
 qed "rtrancl_idemp_self_comp";
 Addsimps [rtrancl_idemp_self_comp];
 
@@ -153,13 +153,13 @@
 Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
+by (blast_tac (claset() addIs rtranclIs) 1);
 qed "rtrancl_converseD";
 
 Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
+by (blast_tac (claset() addIs rtranclIs) 1);
 qed "rtrancl_converseI";
 
 Goal "(r^-1)^* = (r^*)^-1";
@@ -288,7 +288,7 @@
 bind_thm ("trancl_trans", trans_trancl RS transD);
 
 Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
-by (blast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl]) 1);
+by (blast_tac (claset() addIs rtranclIs) 1);
 qed "rtrancl_trancl_trancl";
 
 (* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
diff -r aecb5bf6f76f -r 9d5678e6bf34 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Mon Oct 09 19:20:55 2000 +0200
+++ b/src/HOL/UNITY/Reach.ML	Mon Oct 09 19:49:58 2000 +0200
@@ -31,7 +31,7 @@
 
 Goal "Rprg : Always reach_invariant";
 by (always_tac 1);
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
+by (blast_tac (claset() addIs rtranclIs) 1);
 qed "reach_invariant";
 
 
@@ -42,7 +42,7 @@
      "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
 by (rtac equalityI 1);
 by (auto_tac (claset() addSIs [ext], simpset()));
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
+by (blast_tac (claset() addIs rtranclIs) 2);
 by (etac rtrancl_induct 1);
 by Auto_tac;
 qed "fixedpoint_invariant_correct";