equal
deleted
inserted
replaced
14 [(["Apply"], "[i,i]=>i")])]; |
14 [(["Apply"], "[i,i]=>i")])]; |
15 val rec_styp = "i=>i"; |
15 val rec_styp = "i=>i"; |
16 val ext = None |
16 val ext = None |
17 val sintrs = ["[| a: A; l: list(term(A)) |] ==> Apply(a,l) : term(A)"]; |
17 val sintrs = ["[| a: A; l: list(term(A)) |] ==> Apply(a,l) : term(A)"]; |
18 val monos = [list_mono]; |
18 val monos = [list_mono]; |
19 val type_intrs = data_typechecks; |
19 val type_intrs = datatype_intrs; |
20 val type_elims = [make_elim (list_univ RS subsetD)]); |
20 val type_elims = [make_elim (list_univ RS subsetD)]); |
21 |
21 |
22 val [ApplyI] = Term.intrs; |
22 val [ApplyI] = Term.intrs; |
23 |
23 |
24 (*Induction on term(A) followed by induction on List *) |
24 (*Induction on term(A) followed by induction on List *) |