document 'locale_deps';
authorwenzelm
Fri Jan 04 12:44:47 2013 +0100 (2013-01-04)
changeset 50716e04c44dc11fc
parent 50715 8cfd585b9162
child 50717 30bcdd5c8e78
document 'locale_deps';
NEWS
src/Doc/IsarRef/Spec.thy
     1.1 --- a/NEWS	Fri Jan 04 12:33:25 2013 +0100
     1.2 +++ b/NEWS	Fri Jan 04 12:44:47 2013 +0100
     1.3 @@ -123,6 +123,9 @@
     1.4  
     1.5    typ "_ * _ * bool * unit" :: finite
     1.6  
     1.7 +* Command 'locale_deps' visualizes all locales and their relations as
     1.8 +a Hasse diagram.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  
     2.1 --- a/src/Doc/IsarRef/Spec.thy	Fri Jan 04 12:33:25 2013 +0100
     2.2 +++ b/src/Doc/IsarRef/Spec.thy	Fri Jan 04 12:44:47 2013 +0100
     2.3 @@ -459,6 +459,7 @@
     2.4      @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
     2.5      @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     2.6      @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     2.7 +    @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     2.8      @{method_def intro_locales} & : & @{text method} \\
     2.9      @{method_def unfold_locales} & : & @{text method} \\
    2.10    \end{matharray}
    2.11 @@ -572,6 +573,10 @@
    2.12    \item @{command "print_locales"} prints the names of all locales
    2.13    of the current theory.
    2.14  
    2.15 +  \item @{command "locale_deps"} visualizes all locales and their
    2.16 +  relations as a Hasse diagram. This includes locales defined as type
    2.17 +  classes (\secref{sec:class}).
    2.18 +
    2.19    \item @{method intro_locales} and @{method unfold_locales}
    2.20    repeatedly expand all introduction rules of locale predicates of the
    2.21    theory.  While @{method intro_locales} only applies the @{text