src/HOL/WF.ML
changeset 4059 59c1422c9da5
parent 3919 c036caebfc75
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/WF.ML	Sat Nov 01 12:58:08 1997 +0100
     1.2 +++ b/src/HOL/WF.ML	Sat Nov 01 12:59:06 1997 +0100
     1.3 @@ -121,9 +121,10 @@
     1.4   by (Blast_tac 2);
     1.5  by (case_tac "y:Q" 1);
     1.6   by (Blast_tac 2);
     1.7 -by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
     1.8 +by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
     1.9   by (assume_tac 1);
    1.10 -by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    1.11 +by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1);	(*essential for speed*)
    1.12 +by (blast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    1.13  qed "wf_insert";
    1.14  AddIffs [wf_insert];
    1.15