doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 26854 9b4aec46ad78
parent 26852 a31203f58b20
child 26861 e6fe036ec21d
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 22:17:37 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 22:20:33 2008 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4  \begin{isamarkuptext}%
     1.5  \begin{matharray}{rcl}
     1.6      \indexdef{HOL}{command}{datatype}\mbox{\isa{\isacommand{datatype}}} & : & \isartrans{theory}{theory} \\
     1.7 -    \indexdef{HOL}{command}{rep-datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
     1.8 +    \indexdef{HOL}{command}{rep\_datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12 @@ -517,9 +517,9 @@
    1.13  %
    1.14  \begin{isamarkuptext}%
    1.15  \begin{matharray}{rcl}
    1.16 -    \indexdef{HOL}{method}{pat-completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
    1.17 +    \indexdef{HOL}{method}{pat\_completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
    1.18      \indexdef{HOL}{method}{relation}\mbox{\isa{relation}} & : & \isarmeth \\
    1.19 -    \indexdef{HOL}{method}{lexicographic-order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
    1.20 +    \indexdef{HOL}{method}{lexicographic\_order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
    1.21    \end{matharray}
    1.22  
    1.23    \begin{rail}
    1.24 @@ -567,7 +567,7 @@
    1.25  
    1.26    \begin{matharray}{rcl}
    1.27      \indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\
    1.28 -    \indexdef{HOL}{command}{recdef-tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
    1.29 +    \indexdef{HOL}{command}{recdef\_tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
    1.30    \end{matharray}
    1.31  
    1.32    \begin{rail}
    1.33 @@ -609,9 +609,9 @@
    1.34    globally, using the following attributes.
    1.35  
    1.36    \begin{matharray}{rcl}
    1.37 -    \indexdef{HOL}{attribute}{recdef-simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
    1.38 -    \indexdef{HOL}{attribute}{recdef-cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
    1.39 -    \indexdef{HOL}{attribute}{recdef-wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
    1.40 +    \indexdef{HOL}{attribute}{recdef\_simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
    1.41 +    \indexdef{HOL}{attribute}{recdef\_cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
    1.42 +    \indexdef{HOL}{attribute}{recdef\_wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
    1.43    \end{matharray}
    1.44  
    1.45    \begin{rail}
    1.46 @@ -628,7 +628,7 @@
    1.47  \begin{isamarkuptext}%
    1.48  \begin{matharray}{rcl}
    1.49      \indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\
    1.50 -    \indexdef{HOL}{command}{ax-specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
    1.51 +    \indexdef{HOL}{command}{ax\_specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
    1.52    \end{matharray}
    1.53  
    1.54    \begin{rail}
    1.55 @@ -698,9 +698,9 @@
    1.56  
    1.57    \begin{matharray}{rcl}
    1.58      \indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\
    1.59 -    \indexdef{HOL}{command}{inductive-set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    1.60 +    \indexdef{HOL}{command}{inductive\_set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    1.61      \indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\
    1.62 -    \indexdef{HOL}{command}{coinductive-set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    1.63 +    \indexdef{HOL}{command}{coinductive\_set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    1.64      \indexdef{HOL}{attribute}{mono}\mbox{\isa{mono}} & : & \isaratt \\
    1.65    \end{matharray}
    1.66  
    1.67 @@ -817,7 +817,7 @@
    1.68  \begin{isamarkuptext}%
    1.69  \begin{matharray}{rcl}
    1.70      \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
    1.71 -    \indexdef{HOL}{method}{arith-split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
    1.72 +    \indexdef{HOL}{method}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
    1.73    \end{matharray}
    1.74  
    1.75    The \mbox{\isa{arith}} method decides linear arithmetic problems
    1.76 @@ -841,10 +841,10 @@
    1.77    ported to Isar.  These should be never used in proper proof texts!
    1.78  
    1.79    \begin{matharray}{rcl}
    1.80 -    \indexdef{HOL}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.81 -    \indexdef{HOL}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.82 -    \indexdef{HOL}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.83 -    \indexdef{HOL}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
    1.84 +    \indexdef{HOL}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.85 +    \indexdef{HOL}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.86 +    \indexdef{HOL}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.87 +    \indexdef{HOL}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
    1.88    \end{matharray}
    1.89  
    1.90    \begin{rail}
    1.91 @@ -900,10 +900,10 @@
    1.92  
    1.93    \begin{matharray}{rcl}
    1.94      \indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    1.95 -    \indexdef{HOL}{command}{code-module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
    1.96 -    \indexdef{HOL}{command}{code-library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
    1.97 -    \indexdef{HOL}{command}{consts-code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
    1.98 -    \indexdef{HOL}{command}{types-code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\  
    1.99 +    \indexdef{HOL}{command}{code\_module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
   1.100 +    \indexdef{HOL}{command}{code\_library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
   1.101 +    \indexdef{HOL}{command}{consts\_code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
   1.102 +    \indexdef{HOL}{command}{types\_code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\  
   1.103      \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
   1.104    \end{matharray}
   1.105  
   1.106 @@ -961,20 +961,20 @@
   1.107    introduction on how to use it.
   1.108  
   1.109    \begin{matharray}{rcl}
   1.110 -    \indexdef{HOL}{command}{export-code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.111 -    \indexdef{HOL}{command}{code-thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.112 -    \indexdef{HOL}{command}{code-deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.113 -    \indexdef{HOL}{command}{code-datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
   1.114 -    \indexdef{HOL}{command}{code-const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
   1.115 -    \indexdef{HOL}{command}{code-type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
   1.116 -    \indexdef{HOL}{command}{code-class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
   1.117 -    \indexdef{HOL}{command}{code-instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
   1.118 -    \indexdef{HOL}{command}{code-monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
   1.119 -    \indexdef{HOL}{command}{code-reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
   1.120 -    \indexdef{HOL}{command}{code-include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
   1.121 -    \indexdef{HOL}{command}{code-modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
   1.122 -    \indexdef{HOL}{command}{code-exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
   1.123 -    \indexdef{HOL}{command}{print-codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.124 +    \indexdef{HOL}{command}{export\_code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.125 +    \indexdef{HOL}{command}{code\_thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.126 +    \indexdef{HOL}{command}{code\_deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.127 +    \indexdef{HOL}{command}{code\_datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
   1.128 +    \indexdef{HOL}{command}{code\_const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
   1.129 +    \indexdef{HOL}{command}{code\_type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
   1.130 +    \indexdef{HOL}{command}{code\_class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
   1.131 +    \indexdef{HOL}{command}{code\_instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
   1.132 +    \indexdef{HOL}{command}{code\_monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
   1.133 +    \indexdef{HOL}{command}{code\_reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
   1.134 +    \indexdef{HOL}{command}{code\_include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
   1.135 +    \indexdef{HOL}{command}{code\_modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
   1.136 +    \indexdef{HOL}{command}{code\_exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
   1.137 +    \indexdef{HOL}{command}{print\_codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.138      \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
   1.139    \end{matharray}
   1.140