80 |
80 |
81 \item[$arities$] is a series of type arity declarations. Each assigns |
81 \item[$arities$] is a series of type arity declarations. Each assigns |
82 arities to type constructors. The $name$ must be an existing type |
82 arities to type constructors. The $name$ must be an existing type |
83 constructor, which is given the additional arity $arity$. |
83 constructor, which is given the additional arity $arity$. |
84 |
84 |
|
85 \item[$nonterminals$]\index{*nonterminal symbols} declares purely |
|
86 syntactic types to be used as nonterminal symbols of the context |
|
87 free grammar. |
|
88 |
85 \item[$consts$] is a series of constant declarations. Each new |
89 \item[$consts$] is a series of constant declarations. Each new |
86 constant $name$ is given the specified type. The optional $mixfix$ |
90 constant $name$ is given the specified type. The optional $mixfix$ |
87 annotations may attach concrete syntax to the constant. |
91 annotations may attach concrete syntax to the constant. |
88 |
92 |
89 \item[$syntax$] \index{*syntax section}\index{print mode} is a variant |
93 \item[$syntax$] \index{*syntax section}\index{print mode} is a variant |
145 |
149 |
146 \item[$oracle$] links the theory to a trusted external reasoner. It is |
150 \item[$oracle$] links the theory to a trusted external reasoner. It is |
147 allowed to create theorems, but each theorem carries a proof object |
151 allowed to create theorems, but each theorem carries a proof object |
148 describing the oracle invocation. See \S\ref{sec:oracles} for details. |
152 describing the oracle invocation. See \S\ref{sec:oracles} for details. |
149 |
153 |
150 \item[$local, global$] changes the current name declaration mode. |
154 \item[$local$, $global$] change the current name declaration mode. |
151 Initially, theories start in $local$ mode, causing all names of |
155 Initially, theories start in $local$ mode, causing all names of |
152 types, constants, axioms etc.\ to be automatically qualified by the |
156 types, constants, axioms etc.\ to be automatically qualified by the |
153 theory name. Changing this to $global$ causes all names to be |
157 theory name. Changing this to $global$ causes all names to be |
154 declared as short base names only. |
158 declared as short base names only. |
155 |
159 |
156 The $local$ and $global$ declarations act like switches, affecting |
160 The $local$ and $global$ declarations act like switches, affecting |
157 all following theory sections until changed again explicitly. Also |
161 all following theory sections until changed again explicitly. Also |
158 note that the final state at the end of the theory will persist. In |
162 note that the final state at the end of the theory will persist. In |
159 particular, this determines how the names of theorems stored later |
163 particular, this determines how the names of theorems stored later |
160 on are handled. |
164 on are handled. |
|
165 |
|
166 \item[$setup$]\index{*setup!theory} applies a list of ML functions to |
|
167 the theory. The argument should denote a value of type |
|
168 \texttt{(theory -> theory) list}. Typically, ML packages are |
|
169 initialized in this way. |
161 |
170 |
162 \item[$ml$] \index{*ML section} |
171 \item[$ml$] \index{*ML section} |
163 consists of \ML\ code, typically for parse and print translation functions. |
172 consists of \ML\ code, typically for parse and print translation functions. |
164 \end{description} |
173 \end{description} |
165 % |
174 % |
527 \subsection{Inspecting a theory}\label{sec:inspct-thy} |
536 \subsection{Inspecting a theory}\label{sec:inspct-thy} |
528 \index{theories!inspecting|bold} |
537 \index{theories!inspecting|bold} |
529 \begin{ttbox} |
538 \begin{ttbox} |
530 print_syntax : theory -> unit |
539 print_syntax : theory -> unit |
531 print_theory : theory -> unit |
540 print_theory : theory -> unit |
532 print_data : theory -> string -> unit |
|
533 parents_of : theory -> theory list |
541 parents_of : theory -> theory list |
534 ancestors_of : theory -> theory list |
542 ancestors_of : theory -> theory list |
535 sign_of : theory -> Sign.sg |
543 sign_of : theory -> Sign.sg |
536 Sign.stamp_names_of : Sign.sg -> string list |
544 Sign.stamp_names_of : Sign.sg -> string list |
537 \end{ttbox} |
545 \end{ttbox} |
541 (grammar, macros, translation functions etc., see |
549 (grammar, macros, translation functions etc., see |
542 page~\pageref{pg:print_syn} for more details). |
550 page~\pageref{pg:print_syn} for more details). |
543 |
551 |
544 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of |
552 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of |
545 $thy$, excluding the syntax. |
553 $thy$, excluding the syntax. |
546 |
|
547 \item[\ttindexbold{print_data} $thy$ $kind$] prints generic data of |
|
548 $thy$. This invokes the print method associated with $kind$. Refer |
|
549 to the output of \texttt{print_theory} for a list of available data |
|
550 kinds in $thy$. |
|
551 |
554 |
552 \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors |
555 \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors |
553 of~$thy$. |
556 of~$thy$. |
554 |
557 |
555 \item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$ |
558 \item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$ |