equal
deleted
inserted
replaced
499 subsection \<open>Locale declarations\<close> |
499 subsection \<open>Locale declarations\<close> |
500 |
500 |
501 text \<open> |
501 text \<open> |
502 \begin{matharray}{rcl} |
502 \begin{matharray}{rcl} |
503 @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
503 @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
|
504 @{command_def "experiment"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
504 @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
505 @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
505 @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
506 @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
506 @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
507 @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
507 @{method_def intro_locales} & : & @{text method} \\ |
508 @{method_def intro_locales} & : & @{text method} \\ |
508 @{method_def unfold_locales} & : & @{text method} \\ |
509 @{method_def unfold_locales} & : & @{text method} \\ |
510 |
511 |
511 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
512 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
512 \indexisarelem{defines}\indexisarelem{notes} |
513 \indexisarelem{defines}\indexisarelem{notes} |
513 @{rail \<open> |
514 @{rail \<open> |
514 @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'? |
515 @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'? |
|
516 ; |
|
517 @@{command experiment} (@{syntax context_elem}*) @'begin' |
515 ; |
518 ; |
516 @@{command print_locale} '!'? @{syntax nameref} |
519 @@{command print_locale} '!'? @{syntax nameref} |
517 ; |
520 ; |
518 @{syntax_def locale}: @{syntax context_elem}+ | |
521 @{syntax_def locale}: @{syntax context_elem}+ | |
519 @{syntax locale_expr} ('+' (@{syntax context_elem}+))? |
522 @{syntax locale_expr} ('+' (@{syntax context_elem}+))? |
608 packages attempts to internalize statements according to the |
611 packages attempts to internalize statements according to the |
609 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and |
612 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and |
610 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also |
613 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also |
611 \secref{sec:object-logic}). Separate introduction rules @{text |
614 \secref{sec:object-logic}). Separate introduction rules @{text |
612 loc_axioms.intro} and @{text loc.intro} are provided as well. |
615 loc_axioms.intro} and @{text loc.intro} are provided as well. |
613 |
616 |
|
617 \item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an |
|
618 anonymous locale context with private naming policy. Specifications in its |
|
619 body are inaccessible from outside. This is useful to perform experiments, |
|
620 without polluting the name space. |
|
621 |
614 \item @{command "print_locale"}~@{text "locale"} prints the |
622 \item @{command "print_locale"}~@{text "locale"} prints the |
615 contents of the named locale. The command omits @{element "notes"} |
623 contents of the named locale. The command omits @{element "notes"} |
616 elements by default. Use @{command "print_locale"}@{text "!"} to |
624 elements by default. Use @{command "print_locale"}@{text "!"} to |
617 have them included. |
625 have them included. |
618 |
626 |