doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 40255 9ffbc25e1606
parent 40254 6d1ebaa7a4ba
child 40388 cb9fd7dd641c
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -72,7 +72,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 @@ -355,7 +355,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 @@ -501,9 +501,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 @@ -633,7 +633,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 @@ -672,7 +672,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  *}
    1.51 @@ -712,7 +712,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 @@ -991,13 +991,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 @@ -1078,8 +1078,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 @@ -1101,10 +1101,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 @@ -1113,41 +1113,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 @@ -1281,7 +1281,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 @@ -1289,13 +1289,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 @@ -1326,7 +1326,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}