src/HOL/WF.ML
changeset 4750 f83cd6a06676
parent 4746 a5dcd7e4a37d
child 4762 afebaa81f148
     1.1 --- a/src/HOL/WF.ML	Tue Mar 24 15:46:08 1998 +0100
     1.2 +++ b/src/HOL/WF.ML	Tue Mar 24 15:46:34 1998 +0100
     1.3 @@ -131,6 +131,9 @@
     1.4  
     1.5  (*** acyclic ***)
     1.6  
     1.7 +val acyclicI = prove_goalw WF.thy [acyclic_def] 
     1.8 +"!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]);
     1.9 +
    1.10  goalw WF.thy [acyclic_def]
    1.11   "!!r. wf r ==> acyclic r";
    1.12  by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);