equal
deleted
inserted
replaced
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 Toplevel.begin_local_theory begin |
375 (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin))); |
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 |
380 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr |
380 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr |
418 (K.tag_proof K.prf_goal) |
418 (K.tag_proof K.prf_goal) |
419 (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); |
419 (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); |
420 |
420 |
421 val showP = |
421 val showP = |
422 OuterSyntax.command "show" "state local goal, solving current obligation" |
422 OuterSyntax.command "show" "state local goal, solving current obligation" |
423 (K.tag_proof K.prf_goal) |
423 (K.tag_proof K.prf_asm_goal) |
424 (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); |
424 (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); |
425 |
425 |
426 val thusP = |
426 val thusP = |
427 OuterSyntax.command "thus" "abbreviates \"then show\"" |
427 OuterSyntax.command "thus" "abbreviates \"then show\"" |
428 (K.tag_proof K.prf_goal) |
428 (K.tag_proof K.prf_asm_goal) |
429 (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); |
429 (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); |
430 |
430 |
431 |
431 |
432 (* facts *) |
432 (* facts *) |
433 |
433 |