Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/Transition.ML
changeset 3023 01364e2f30ad
parent 2637 e9b203f854ae
child 3439 54785105178c 
--- a/src/HOL/IMP/Transition.ML	Wed Apr 23 11:12:10 1997 +0200
+++ b/src/HOL/IMP/Transition.ML	Wed Apr 23 11:18:29 1997 +0200
@@ -194,7 +194,7 @@
 goal Transition.thy 
   "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
 by (etac evalc1.induct 1);
-auto();
+by (Auto_tac());
 qed_spec_mp "FB_lemma3";
 
 val [major] = goal Transition.thy
isabelle