equal
deleted
inserted
replaced
26 |
26 |
27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); |
27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); |
28 |
28 |
29 print_depth 1; |
29 print_depth 1; |
30 |
30 |
|
31 (*Add user sections for inductive/datatype definitions*) |
|
32 use_thy "Datatype"; |
|
33 structure ThySyn = ThySynFun |
|
34 (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", |
|
35 "and", "|", "<=", "domains", "intrs", "monos", |
|
36 "con_defs", "type_intrs", "type_elims"] |
|
37 and user_sections = [("inductive", inductive_decl ""), |
|
38 ("coinductive", inductive_decl "Co"), |
|
39 ("datatype", datatype_decl ""), |
|
40 ("codatatype", datatype_decl "Co")]); |
|
41 init_thy_reader (); |
|
42 |
31 use_thy "InfDatatype"; |
43 use_thy "InfDatatype"; |
32 use_thy "ListFn"; |
44 use_thy "List"; |
33 |
45 |
34 (*printing functions are inherited from FOL*) |
46 (*printing functions are inherited from FOL*) |
35 print_depth 8; |
47 print_depth 8; |
36 |
48 |
37 val ZF_build_completed = (); (*indicate successful build*) |
49 val ZF_build_completed = (); (*indicate successful build*) |