test.ML
author lcp
Wed, 01 Dec 1993 13:05:25 +0100
changeset 22 17b6487e1ac7
parent 0 7949f97df77a
permissions -rw-r--r--
HOL/llist/LList_corec_subset1: does not need induction

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;