test.ML

INSTALLATION OF INDUCTIVE DEFINITIONS
HOL/ex/MT.thy: now mentions dependence upon Sum.thy
HOL/ex/Acc: new example, borrowed & adapted from ZF
HOL/ex/Simult, ex/Term: updated refs to Sexp intr rules
HOL/Sexp,List,LList,ex/Term: converted as follows
node *set -> item
Sexp -> sexp
LList_corec -> <self>
LList_ -> llist_
LList\> -> llist
List_case -> <self>
List_rec -> <self>
List_ -> list_
List\> -> list
Term_rec -> <self>
Term_ -> term_
Term\> -> term

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;