theory Commands imports Main
keywords "print_test" :: diag and "global_test" :: thy_decl and "local_test" :: thy_decl begin
subsection \<open>Diagnostic command: no state change\<close>
ML \<open>
Outer_Syntax.command \<^command_keyword>\<open>print_test\<close> "print term test"
(Parse.term >> (fn s => Toplevel.keep (fn st => let
val ctxt = Toplevel.context_of st;
val t = Syntax.read_term ctxt s;
val ctxt' = Proof_Context.augment t ctxt; in Pretty.writeln (Syntax.pretty_term ctxt' t) end))); \<close>
print_test x
print_test "\x. x = a"
subsection \<open>Old-style global theory declaration\<close>
ML \<open>
Outer_Syntax.command \<^command_keyword>\<open>global_test\<close> "test constant declaration"
(Parse.binding >> (fn b => Toplevel.theory (fn thy => let
val thy' = Sign.add_consts [(b, \<^typ>\'a\, NoSyn)] thy; in thy' end))); \<close>
global_test a
global_test b
print_test a
subsection \<open>Local theory specification\<close>
ML \<open>
Outer_Syntax.local_theory \<^command_keyword>\<open>local_test\<close> "test local definition"
(Parse.binding -- (\<^keyword>\<open>=\<close> |-- Parse.term) >> (fn (b, s) => fn lthy => let
val t = Syntax.read_term lthy s;
val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy; in lthy' end)); \<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
