diff -r 000000000000 -r 7949f97df77a test.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test.ML	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,6 @@
+let
+ fun tac ss = resolve_tac(prems_of_ss ss) ORELSE' asm_simp_tac ss;
+ val ss = set_prove_tac(HOL_ss addsimps [Suc_lessD],tac)
+in prove_goal Nat.thy "!!x. Suc(Suc(Suc(x)))<y ==> x<y"
+     (fn _ => [asm_simp_tac ss 1])
+end;