src/HOL/WF.ML
changeset 4762 afebaa81f148
parent 4750 f83cd6a06676
child 4821 bfbaea156f43
     1.1 --- a/src/HOL/WF.ML	Mon Mar 30 21:06:09 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Mon Mar 30 21:08:05 1998 +0200
     1.3 @@ -63,6 +63,11 @@
     1.4  qed "wf_trancl";
     1.5  
     1.6  
     1.7 +val wf_converse_trancl = prove_goal thy 
     1.8 +"!!X. wf (r^-1) ==> wf ((r^+)^-1)" (K [
     1.9 +	stac (trancl_converse RS sym) 1,
    1.10 +	etac wf_trancl 1]);
    1.11 +
    1.12  (*----------------------------------------------------------------------------
    1.13   * Minimal-element characterization of well-foundedness
    1.14   *---------------------------------------------------------------------------*)
    1.15 @@ -285,10 +290,10 @@
    1.16  by (rtac trans_trancl 1);
    1.17  by (rtac transD 1);
    1.18  by (rtac trans_trancl 1);
    1.19 -by (forw_inst_tac [("a","ya")] r_into_trancl 1);
    1.20 +by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1);
    1.21  by (atac 1);
    1.22  by (atac 1);
    1.23 -by (forw_inst_tac [("a","ya")] r_into_trancl 1);
    1.24 +by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1);
    1.25  by (atac 1);
    1.26  qed "wfrec";
    1.27