1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 29 11:35:47 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 29 11:49:56 2010 +0200
1.3 @@ -93,7 +93,7 @@
1.4 \end{matharray}
1.5
1.6 \begin{rail}
1.7 - 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
1.8 + 'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
1.9 ;
1.10 \end{rail}
1.11
1.12 @@ -364,7 +364,7 @@
1.13 \begin{rail}
1.14 'datatype' (dtspec + 'and')
1.15 ;
1.16 - 'rep\_datatype' ('(' (name +) ')')? (term +)
1.17 + 'rep_datatype' ('(' (name +) ')')? (term +)
1.18 ;
1.19
1.20 dtspec: parname? typespec mixfix? '=' (cons + '|')
1.21 @@ -511,9 +511,9 @@
1.22 \begin{rail}
1.23 'relation' term
1.24 ;
1.25 - 'lexicographic\_order' ( clasimpmod * )
1.26 + 'lexicographic_order' ( clasimpmod * )
1.27 ;
1.28 - 'size\_change' ( orders ( clasimpmod * ) )
1.29 + 'size_change' ( orders ( clasimpmod * ) )
1.30 ;
1.31 orders: ( 'max' | 'min' | 'ms' ) *
1.32 \end{rail}
1.33 @@ -642,7 +642,7 @@
1.34 ;
1.35 hints: '(' 'hints' ( recdefmod * ) ')'
1.36 ;
1.37 - recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
1.38 + recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
1.39 ;
1.40 tc: nameref ('(' nat ')')?
1.41 ;
1.42 @@ -680,7 +680,7 @@
1.43 \end{matharray}
1.44
1.45 \begin{rail}
1.46 - ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
1.47 + ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
1.48 ;
1.49 \end{rail}%
1.50 \end{isamarkuptext}%
1.51 @@ -722,7 +722,7 @@
1.52 \end{matharray}
1.53
1.54 \begin{rail}
1.55 - ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
1.56 + ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
1.57 ('where' clauses)? ('monos' thmrefs)?
1.58 ;
1.59 clauses: (thmdecl? prop + '|')
1.60 @@ -1010,13 +1010,13 @@
1.61 \end{matharray}
1.62
1.63 \begin{rail}
1.64 - 'case\_tac' goalspec? term rule?
1.65 + 'case_tac' goalspec? term rule?
1.66 ;
1.67 - 'induct\_tac' goalspec? (insts * 'and') rule?
1.68 + 'induct_tac' goalspec? (insts * 'and') rule?
1.69 ;
1.70 - 'ind\_cases' (prop +) ('for' (name +)) ?
1.71 + 'ind_cases' (prop +) ('for' (name +)) ?
1.72 ;
1.73 - 'inductive\_cases' (thmdecl? (prop +) + 'and')
1.74 + 'inductive_cases' (thmdecl? (prop +) + 'and')
1.75 ;
1.76
1.77 rule: ('rule' ':' thmref)
1.78 @@ -1093,8 +1093,8 @@
1.79 \end{matharray}
1.80
1.81 \begin{rail}
1.82 - 'export\_code' ( constexpr + ) \\
1.83 - ( ( 'in' target ( 'module\_name' string ) ? \\
1.84 + 'export_code' ( constexpr + ) \\
1.85 + ( ( 'in' target ( 'module_name' string ) ? \\
1.86 ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1.87 ;
1.88
1.89 @@ -1116,10 +1116,10 @@
1.90 'code' ( 'del' | 'abstype' | 'abstract' ) ?
1.91 ;
1.92
1.93 - 'code\_abort' ( const + )
1.94 + 'code_abort' ( const + )
1.95 ;
1.96
1.97 - 'code\_datatype' ( const + )
1.98 + 'code_datatype' ( const + )
1.99 ;
1.100
1.101 'code_inline' ( 'del' ) ?
1.102 @@ -1128,41 +1128,41 @@
1.103 'code_post' ( 'del' ) ?
1.104 ;
1.105
1.106 - 'code\_thms' ( constexpr + ) ?
1.107 + 'code_thms' ( constexpr + ) ?
1.108 ;
1.109
1.110 - 'code\_deps' ( constexpr + ) ?
1.111 + 'code_deps' ( constexpr + ) ?
1.112 ;
1.113
1.114 - 'code\_const' (const + 'and') \\
1.115 + 'code_const' (const + 'and') \\
1.116 ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.117 ;
1.118
1.119 - 'code\_type' (typeconstructor + 'and') \\
1.120 + 'code_type' (typeconstructor + 'and') \\
1.121 ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.122 ;
1.123
1.124 - 'code\_class' (class + 'and') \\
1.125 + 'code_class' (class + 'and') \\
1.126 ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
1.127 ;
1.128
1.129 - 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
1.130 + 'code_instance' (( typeconstructor '::' class ) + 'and') \\
1.131 ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
1.132 ;
1.133
1.134 - 'code\_reserved' target ( string + )
1.135 + 'code_reserved' target ( string + )
1.136 ;
1.137
1.138 - 'code\_monad' const const target
1.139 + 'code_monad' const const target
1.140 ;
1.141
1.142 - 'code\_include' target ( string ( string | '-') )
1.143 + 'code_include' target ( string ( string | '-') )
1.144 ;
1.145
1.146 - 'code\_modulename' target ( ( string string ) + )
1.147 + 'code_modulename' target ( ( string string ) + )
1.148 ;
1.149
1.150 - 'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
1.151 + 'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
1.152 ( 'functions' ( string + ) ) ? ( 'file' string ) ?
1.153 ;
1.154
1.155 @@ -1293,7 +1293,7 @@
1.156 \end{matharray}
1.157
1.158 \begin{rail}
1.159 - ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
1.160 + ( 'code_module' | 'code_library' ) modespec ? name ? \\
1.161 ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
1.162 'contains' ( ( name '=' term ) + | term + )
1.163 ;
1.164 @@ -1301,13 +1301,13 @@
1.165 modespec: '(' ( name * ) ')'
1.166 ;
1.167
1.168 - 'consts\_code' (codespec +)
1.169 + 'consts_code' (codespec +)
1.170 ;
1.171
1.172 codespec: const template attachment ?
1.173 ;
1.174
1.175 - 'types\_code' (tycodespec +)
1.176 + 'types_code' (tycodespec +)
1.177 ;
1.178
1.179 tycodespec: name template attachment ?
1.180 @@ -1339,7 +1339,7 @@
1.181 \end{matharray}
1.182
1.183 \begin{rail}
1.184 - ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
1.185 + ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
1.186 ;
1.187 decl: ((name ':')? term '(' 'overloaded' ')'?)
1.188 \end{rail}