equal
deleted
inserted
replaced
163 val tmp_thy = Theory.copy thy |
163 val tmp_thy = Theory.copy thy |
164 val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn) |
164 val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn) |
165 val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy |
165 val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy |
166 val trm1 = Syntax.read_term_global tmp_thy' "FOO baz" |
166 val trm1 = Syntax.read_term_global tmp_thy' "FOO baz" |
167 val trm2 = Syntax.read_term_global thy "FOO baz" |
167 val trm2 = Syntax.read_term_global thy "FOO baz" |
168 val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2) |
168 val _ = pwriteln |
|
169 (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)) |
169 in |
170 in |
170 thy |
171 thy |
171 end *} |
172 end *} |
172 |
173 |
173 text {* |
174 text {* |
190 There are two reasons for parsing a term in a temporary theory. One is to |
191 There are two reasons for parsing a term in a temporary theory. One is to |
191 obtain fully qualified names for constants and the other is appropriate type |
192 obtain fully qualified names for constants and the other is appropriate type |
192 inference. This is relevant in situations where definitions are made later, |
193 inference. This is relevant in situations where definitions are made later, |
193 but parsing and type inference has to take already proceed as if the definitions |
194 but parsing and type inference has to take already proceed as if the definitions |
194 were already made. |
195 were already made. |
|
196 |
|
197 \begin{readmore} |
|
198 Most of the functions about theories are implemented in |
|
199 @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}. |
|
200 \end{readmore} |
195 *} |
201 *} |
196 |
202 |
197 section {* Contexts *} |
203 section {* Contexts *} |
198 |
204 |
199 text {* |
205 text {* |
313 "@{context} |
319 "@{context} |
314 |> Variable.variant_fixes [\"y\", \"y\", \"z\"]" |
320 |> Variable.variant_fixes [\"y\", \"y\", \"z\"]" |
315 "([\"y\", \"ya\", \"z\"], ...)"} |
321 "([\"y\", \"ya\", \"z\"], ...)"} |
316 |
322 |
317 Now a fresh variant for the second occurence of @{text y} is created |
323 Now a fresh variant for the second occurence of @{text y} is created |
318 avoiding any clash. In this way we can also create free variables |
324 avoiding any clash. In this way we can also create fresh free variables |
319 that avoid any clashes with fixed variables. In Line~3 below we fix |
325 that avoid any clashes with fixed variables. In Line~3 below we fix |
320 the variable @{text x} in the context @{text ctxt1}. Next we want to |
326 the variable @{text x} in the context @{text ctxt1}. Next we want to |
321 create two fresh variables of type @{typ nat} as variants of the |
327 create two fresh variables of type @{typ nat} as variants of the |
322 string @{text [quotes] "x"} (Lines 6 and 7). |
328 string @{text [quotes] "x"} (Lines 6 and 7). |
323 |
329 |
457 in |
463 in |
458 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
464 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
459 end" |
465 end" |
460 "?P ?x ?y ?z ?x ?y ?z"} |
466 "?P ?x ?y ?z ?x ?y ?z"} |
461 |
467 |
462 Since we fixed all variables in @{text ctxt1}, in the result all of them |
468 Since we fixed all variables in @{text ctxt1}, in the exported |
463 are schematic. The great point of contexts is that exporting from one to |
469 result all of them are schematic. The great point of contexts is |
464 another is not just concerned with variables, but also assumptions. For this we |
470 that exporting from one to another is not just restricted to |
465 can use the function @{ML_ind export in Assumption} from the structure |
471 variables, but also works with assumptions. For this we can use the |
|
472 function @{ML_ind export in Assumption} from the structure |
466 @{ML_struct Assumption}. Consider the following code. |
473 @{ML_struct Assumption}. Consider the following code. |
467 |
474 |
468 @{ML_response_fake [display, gray, linenos] |
475 @{ML_response_fake [display, gray, linenos] |
469 "let |
476 "let |
470 val ctxt0 = @{context} |
477 val ctxt0 = @{context} |
550 thm this |
557 thm this |
551 |
558 |
552 oops |
559 oops |
553 *) |
560 *) |
554 |
561 |
555 section {* Local Theories (TBD) *} |
562 section {* Local Theories and Local Setups\label{sec:local} (TBD) *} |
556 |
563 |
557 text {* |
564 text {* |
558 In contrast to an ordinary theory, which simply consists of a type |
565 In contrast to an ordinary theory, which simply consists of a type |
559 signature, as well as tables for constants, axioms and theorems, a local |
566 signature, as well as tables for constants, axioms and theorems, a local |
560 theory contains additional context information, such as locally fixed |
567 theory contains additional context information, such as locally fixed |