author | nipkow |
Mon, 11 Dec 1995 11:24:51 +0100 | |
changeset 1402 | b72ccd1cff02 |
parent 797 | 713efca1f0aa |
child 1418 | f5f97ee67cbb |
permissions | -rw-r--r-- |
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
1 |
(* Title: ZF/thy_syntax.ML |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
2 |
ID: $Id$ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
4 |
Copyright 1994 University of Cambridge |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
5 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
6 |
Additional theory file sections for ZF |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
7 |
*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
8 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
9 |
structure ThySynData: THY_SYN_DATA = |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
10 |
struct |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
11 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
12 |
(*Inductive definitions theory section. co is either "" or "Co"*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
13 |
fun inductive_decl co = |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
14 |
let open ThyParse |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
15 |
fun mk_intr_name (s,_) = (*the "op" cancels any infix status*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
16 |
if Syntax.is_identifier s then "op " ^ s else "_" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
17 |
fun mk_params ((((((rec_tms, sdom_sum), ipairs), |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
18 |
monos), con_defs), type_intrs), type_elims) = |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
19 |
let val big_rec_name = space_implode "_" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
20 |
(map (scan_to_id o trim) rec_tms) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
21 |
and srec_tms = mk_list rec_tms |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
22 |
and sintrs = mk_big_list (map snd ipairs) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
23 |
val stri_name = big_rec_name ^ "_Intrnl" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
24 |
in |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
25 |
(";\n\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
26 |
\structure " ^ stri_name ^ " =\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
27 |
\ let open Ind_Syntax in\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
28 |
\ struct\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
29 |
\ val _ = writeln \"" ^ co ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
30 |
"Inductive definition " ^ big_rec_name ^ "\"\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
31 |
\ val rec_tms\t= map (readtm (sign_of thy) iT) " |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
32 |
^ srec_tms ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
33 |
\ and dom_sum\t= readtm (sign_of thy) iT " ^ sdom_sum ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
34 |
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
35 |
^ sintrs ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
36 |
\ end\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
37 |
\ end;\n\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
38 |
\val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
39 |
stri_name ^ ".rec_tms, " ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
40 |
stri_name ^ ".dom_sum, " ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
41 |
stri_name ^ ".intr_tms)" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
42 |
, |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
43 |
"structure " ^ big_rec_name ^ " =\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
44 |
\ struct\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
45 |
\ val _ = writeln \"Proofs for " ^ co ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
46 |
"Inductive definition " ^ big_rec_name ^ "\"\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
47 |
\ structure Result = " ^ co ^ "Ind_section_Fun\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
48 |
\ (open " ^ stri_name ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
49 |
\ val thy\t\t= thy\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
50 |
\ val monos\t\t= " ^ monos ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
51 |
\ val con_defs\t\t= " ^ con_defs ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
52 |
\ val type_intrs\t= " ^ type_intrs ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
53 |
\ val type_elims\t= " ^ type_elims ^ ");\n\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
54 |
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
55 |
\ open Result\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
56 |
\ end\n" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
57 |
) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
58 |
end |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
59 |
val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
60 |
val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
61 |
fun optstring s = optional (s $$-- string) "\"[]\"" >> trim |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
62 |
in domains -- ipairs -- optstring "monos" -- optstring "con_defs" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
63 |
-- optstring "type_intrs" -- optstring "type_elims" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
64 |
>> mk_params |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
65 |
end; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
66 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
67 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
68 |
(*Datatype definitions theory section. co is either "" or "Co"*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
69 |
fun datatype_decl co = |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
70 |
let open ThyParse |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
71 |
(*generate strings*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
72 |
fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z); |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
73 |
val mk_data = mk_list o map mk_const o snd |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
74 |
val mk_scons = mk_big_list o map mk_data |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
75 |
fun mk_intr_name s = (*the "op" cancels any infix status*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
76 |
if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
77 |
fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) = |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
78 |
let val rec_names = map (scan_to_id o trim o fst) rec_pairs |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
79 |
val big_rec_name = space_implode "_" rec_names |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
80 |
and srec_tms = mk_list (map fst rec_pairs) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
81 |
and scons = mk_scons rec_pairs |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
82 |
and sdom_sum = |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
83 |
if dom = "" then co ^ "data_domain rec_tms" (*default*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
84 |
else "readtm (sign_of thy) iT " ^ dom |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
85 |
val stri_name = big_rec_name ^ "_Intrnl" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
86 |
val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
87 |
in |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
88 |
(";\n\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
89 |
\structure " ^ stri_name ^ " =\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
90 |
\ let open Ind_Syntax in\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
91 |
\ struct\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
92 |
\ val _ = writeln \"" ^ co ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
93 |
"Datatype definition " ^ big_rec_name ^ "\"\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
94 |
\ val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
95 |
\ val dom_sum\t= " ^ sdom_sum ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
96 |
\ and con_ty_lists\t= read_constructs (sign_of thy)\n" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
97 |
^ scons ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
98 |
\ val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
99 |
\ end\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
100 |
\ end;\n\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
101 |
\val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
102 |
mk_list (map quote rec_names) ^ ", " ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
103 |
stri_name ^ ".con_ty_lists) \n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
104 |
\ |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
105 |
stri_name ^ ".rec_tms, " ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
106 |
stri_name ^ ".dom_sum, " ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
107 |
stri_name ^ ".intr_tms)" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
108 |
, |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
109 |
"structure " ^ big_rec_name ^ " =\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
110 |
\ struct\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
111 |
\ val _ = writeln \"Proofs for " ^ co ^ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
112 |
"Datatype definition " ^ big_rec_name ^ "\"\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
113 |
\ structure Result = " ^ co ^ "Data_section_Fun\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
114 |
\ (open " ^ stri_name ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
115 |
\ val thy\t\t= thy\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
116 |
\ val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
117 |
\ val monos\t\t= " ^ monos ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
118 |
\ val type_intrs\t= " ^ type_intrs ^ "\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
119 |
\ val type_elims\t= " ^ type_elims ^ ");\n\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
120 |
\ val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
121 |
\ open Result\n\ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
122 |
\ end\n" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
123 |
) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
124 |
end |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
125 |
fun optstring s = optional (s $$-- string) "\"[]\"" >> trim |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
126 |
val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
127 |
val construct = name -- string_list -- opt_mixfix; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
128 |
in optional ("<=" $$-- string) "" -- |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
129 |
enum1 "and" (string --$$ "=" -- enum1 "|" construct) -- |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
130 |
optstring "monos" -- optstring "type_intrs" -- optstring "type_elims" |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
131 |
>> mk_params |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
132 |
end; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
133 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
134 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
135 |
(** Section specifications **) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
136 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
137 |
val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
138 |
"and", "|", "<=", "domains", "intrs", "monos", |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
139 |
"con_defs", "type_intrs", "type_elims"]; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
140 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
141 |
val user_sections = [("inductive", inductive_decl ""), |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
142 |
("coinductive", inductive_decl "Co"), |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
143 |
("datatype", datatype_decl ""), |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
144 |
("codatatype", datatype_decl "Co")]; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
145 |
end; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
146 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
147 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
148 |
structure ThySyn = ThySynFun(ThySynData); |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
149 |
init_thy_reader (); |