equal
deleted
inserted
replaced
18 ["Nil : list(A)", |
18 ["Nil : list(A)", |
19 "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"]; |
19 "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"]; |
20 val monos = []; |
20 val monos = []; |
21 val type_intrs = datatype_intrs |
21 val type_intrs = datatype_intrs |
22 val type_elims = datatype_elims); |
22 val type_elims = datatype_elims); |
|
23 |
|
24 store_theory "List" List.thy; |
23 |
25 |
24 val [NilI, ConsI] = List.intrs; |
26 val [NilI, ConsI] = List.intrs; |
25 |
27 |
26 (*An elimination rule, for type-checking*) |
28 (*An elimination rule, for type-checking*) |
27 val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)"; |
29 val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)"; |