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