src/HOL/WF.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4350 1983e4054fd8
     1.1 --- a/src/HOL/WF.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/WF.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4   by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs
     1.5        [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
     1.6  by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
    1.10  by (etac bexE 1);
    1.11  by (rename_tac "a" 1);
    1.12 @@ -327,5 +327,5 @@
    1.13  
    1.14  goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
    1.15  by (Clarify_tac 1);
    1.16 -be wfrec 1;
    1.17 +by (etac wfrec 1);
    1.18  qed "tfl_wfrec";