updated for latest Blast_tac, which treats equality differently
authorpaulson
Wed Dec 03 10:49:33 1997 +0100 (1997-12-03)
changeset 43501983e4054fd8
parent 4349 50403e5a44c0
child 4351 36b28f78ed1b
updated for latest Blast_tac, which treats equality differently
src/HOL/WF.ML
     1.1 --- a/src/HOL/WF.ML	Wed Dec 03 10:48:16 1997 +0100
     1.2 +++ b/src/HOL/WF.ML	Wed Dec 03 10:49:33 1997 +0100
     1.3 @@ -108,8 +108,8 @@
     1.4  
     1.5  goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
     1.6  by (rtac iffI 1);
     1.7 - by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs
     1.8 -      [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
     1.9 + by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] 
    1.10 +	addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
    1.11  by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
    1.12  by Safe_tac;
    1.13  by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
    1.14 @@ -124,7 +124,8 @@
    1.15  by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
    1.16   by (assume_tac 1);
    1.17  by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1);	(*essential for speed*)
    1.18 -by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
    1.19 +(*Blast_tac with new substOccur fails*)
    1.20 +by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
    1.21  qed "wf_insert";
    1.22  AddIffs [wf_insert];
    1.23