src/HOL/ex/Recdefs.ML
changeset 5655 afd75136b236
parent 5518 654ead0ba4f7
child 6451 bc943acc5fda
--- a/src/HOL/ex/Recdefs.ML	Fri Oct 16 17:32:06 1998 +0200
+++ b/src/HOL/ex/Recdefs.ML	Fri Oct 16 17:32:29 1998 +0200
@@ -23,7 +23,6 @@
 Goal "g x < Suc x";
 by (res_inst_tac [("u","x")] g.induct 1);
 by Auto_tac;
-by (trans_tac 1);
 qed "g_terminates";
 
 Goal "g x = 0";