src/Pure/Isar/isar_syn.ML
changeset 21843 2015be1b6a03
parent 21800 6035bfcd72d8
child 21951 56abe5f3c612
equal deleted inserted replaced
21842:3d8ab6545049 21843:2015be1b6a03
   369   OuterSyntax.command "locale" "define named proof context" K.thy_decl
   369   OuterSyntax.command "locale" "define named proof context" K.thy_decl
   370     ((P.opt_keyword "open" >> not) -- P.name
   370     ((P.opt_keyword "open" >> not) -- P.name
   371         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
   371         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
   372         -- P.opt_begin
   372         -- P.opt_begin
   373       >> (fn (((is_open, name), (expr, elems)), begin) =>
   373       >> (fn (((is_open, name), (expr, elems)), begin) =>
   374           Toplevel.begin_local_theory begin
   374           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   375             (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false)));
   375             (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false)));
   376 
   376 
   377 val interpretationP =
   377 val interpretationP =
   378   OuterSyntax.command "interpretation"
   378   OuterSyntax.command "interpretation"
   379     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
   379     "prove and register interpretation of locale expression in theory or locale" K.thy_goal