Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added acyclicI
authoroheimb
Tue, 24 Mar 1998 15:46:34 +0100
changeset 4750 f83cd6a06676
parent 4749 35b47e36e615
child 4751 6fbd9838ccae
added acyclicI
src/HOL/WF.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle