src/HOL/WF.ML
changeset 4350 1983e4054fd8
parent 4153 e534c4c32d54
child 4686 74a12e86b20b
--- a/src/HOL/WF.ML	Wed Dec 03 10:48:16 1997 +0100
+++ b/src/HOL/WF.ML	Wed Dec 03 10:49:33 1997 +0100
@@ -108,8 +108,8 @@
 
 goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
 by (rtac iffI 1);
- by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs
-      [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
+ by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] 
+	addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
 by Safe_tac;
 by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
@@ -124,7 +124,8 @@
 by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
  by (assume_tac 1);
 by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1);	(*essential for speed*)
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+(*Blast_tac with new substOccur fails*)
+by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
 qed "wf_insert";
 AddIffs [wf_insert];