--- a/doc-src/IsarImplementation/Thy/Logic.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Fri Oct 29 17:38:57 2010 +0200
@@ -201,7 +201,7 @@
;
'sort' sort
;
- ('type\_name' | 'type\_abbrev' | 'nonterminal') nameref
+ ('type_name' | 'type_abbrev' | 'nonterminal') nameref
;
'typ' type
;
@@ -437,7 +437,7 @@
\end{matharray}
\begin{rail}
- ('const\_name' | 'const\_abbrev') nameref
+ ('const_name' | 'const_abbrev') nameref
;
'const' ('(' (type + ',') ')')?
;
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Fri Oct 29 17:38:57 2010 +0200
@@ -218,7 +218,7 @@
;
'sort' sort
;
- ('type\_name' | 'type\_abbrev' | 'nonterminal') nameref
+ ('type_name' | 'type_abbrev' | 'nonterminal') nameref
;
'typ' type
;
@@ -464,7 +464,7 @@
\end{matharray}
\begin{rail}
- ('const\_name' | 'const\_abbrev') nameref
+ ('const_name' | 'const_abbrev') nameref
;
'const' ('(' (type + ',') ')')?
;
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Oct 29 17:38:57 2010 +0200
@@ -84,7 +84,7 @@
\begin{rail}
('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
;
- ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+ ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
;
\end{rail}
@@ -198,10 +198,10 @@
'goals' options |
'subgoals' options |
'prf' options thmrefs |
- 'full\_prf' options thmrefs |
+ 'full_prf' options thmrefs |
'ML' options name |
- 'ML\_type' options name |
- 'ML\_struct' options name
+ 'ML_type' options name |
+ 'ML_struct' options name
;
options: '[' (option * ',') ']'
;
@@ -468,7 +468,7 @@
\end{matharray}
\begin{rail}
- ('display\_drafts' | 'print\_drafts') (name +)
+ ('display_drafts' | 'print_drafts') (name +)
;
\end{rail}
--- a/doc-src/IsarRef/Thy/Generic.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Fri Oct 29 17:38:57 2010 +0200
@@ -284,14 +284,14 @@
\end{matharray}
\begin{rail}
- ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
+ ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
( insts thmref | thmrefs )
;
- 'subgoal\_tac' goalspec? (prop +)
+ 'subgoal_tac' goalspec? (prop +)
;
- 'rename\_tac' goalspec? (name +)
+ 'rename_tac' goalspec? (name +)
;
- 'rotate\_tac' goalspec? int?
+ 'rotate_tac' goalspec? int?
;
('tactic' | 'raw_tactic') text
;
@@ -364,10 +364,10 @@
\indexouternonterm{simpmod}
\begin{rail}
- ('simp' | 'simp\_all') opt? (simpmod *)
+ ('simp' | 'simp_all') opt? (simpmod *)
;
- opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
+ opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
;
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
'split' (() | 'add' | 'del')) ':' thmrefs
@@ -471,7 +471,7 @@
\end{matharray}
\begin{rail}
- 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
+ 'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
;
'simproc' (('add' ':')? | 'del' ':') (name+)
@@ -519,7 +519,7 @@
'simplified' opt? thmrefs?
;
- opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
+ opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
;
\end{rail}
@@ -785,7 +785,7 @@
;
'atomize' ('(' 'full' ')')?
;
- 'rule\_format' ('(' 'noasm' ')')?
+ 'rule_format' ('(' 'noasm' ')')?
;
\end{rail}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 29 17:38:57 2010 +0200
@@ -72,7 +72,7 @@
\end{matharray}
\begin{rail}
- 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+ 'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
;
\end{rail}
@@ -355,7 +355,7 @@
\begin{rail}
'datatype' (dtspec + 'and')
;
- 'rep\_datatype' ('(' (name +) ')')? (term +)
+ 'rep_datatype' ('(' (name +) ')')? (term +)
;
dtspec: parname? typespec mixfix? '=' (cons + '|')
@@ -501,9 +501,9 @@
\begin{rail}
'relation' term
;
- 'lexicographic\_order' ( clasimpmod * )
+ 'lexicographic_order' ( clasimpmod * )
;
- 'size\_change' ( orders ( clasimpmod * ) )
+ 'size_change' ( orders ( clasimpmod * ) )
;
orders: ( 'max' | 'min' | 'ms' ) *
\end{rail}
@@ -633,7 +633,7 @@
;
hints: '(' 'hints' ( recdefmod * ) ')'
;
- recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
+ recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
;
tc: nameref ('(' nat ')')?
;
@@ -672,7 +672,7 @@
\end{matharray}
\begin{rail}
- ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
+ ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
;
\end{rail}
*}
@@ -712,7 +712,7 @@
\end{matharray}
\begin{rail}
- ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
+ ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
('where' clauses)? ('monos' thmrefs)?
;
clauses: (thmdecl? prop + '|')
@@ -941,28 +941,29 @@
\begin{description}
- \item[size] specifies the maximum size of the search space for
- assignment values.
+ \item[@{text size}] specifies the maximum size of the search space
+ for assignment values.
- \item[iterations] sets how many sets of assignments are
- generated for each particular size.
+ \item[@{text iterations}] sets how many sets of assignments are
+ generated for each particular size.
- \item[no\_assms] specifies whether assumptions in
- structured proofs should be ignored.
+ \item[@{text no_assms}] specifies whether assumptions in
+ structured proofs should be ignored.
- \item[timeout] sets the time limit in seconds.
+ \item[@{text timeout}] sets the time limit in seconds.
- \item[default\_type] sets the type(s) generally used to instantiate
- type variables.
+ \item[@{text default_type}] sets the type(s) generally used to
+ instantiate type variables.
- \item[report] if set quickcheck reports how many tests fulfilled
- the preconditions.
+ \item[@{text report}] if set quickcheck reports how many tests
+ fulfilled the preconditions.
- \item[quiet] if not set quickcheck informs about the current size
- for assignment values.
+ \item[@{text quiet}] if not set quickcheck informs about the
+ current size for assignment values.
- \item[expect] can be used to check if the user's expectation was met
- (no\_expectation, no\_counterexample, or counterexample)
+ \item[@{text expect}] can be used to check if the user's
+ expectation was met (@{text no_expectation}, @{text
+ no_counterexample}, or @{text counterexample}).
\end{description}
@@ -990,13 +991,13 @@
\end{matharray}
\begin{rail}
- 'case\_tac' goalspec? term rule?
+ 'case_tac' goalspec? term rule?
;
- 'induct\_tac' goalspec? (insts * 'and') rule?
+ 'induct_tac' goalspec? (insts * 'and') rule?
;
- 'ind\_cases' (prop +) ('for' (name +)) ?
+ 'ind_cases' (prop +) ('for' (name +)) ?
;
- 'inductive\_cases' (thmdecl? (prop +) + 'and')
+ 'inductive_cases' (thmdecl? (prop +) + 'and')
;
rule: ('rule' ':' thmref)
@@ -1077,8 +1078,8 @@
\end{matharray}
\begin{rail}
- 'export\_code' ( constexpr + ) \\
- ( ( 'in' target ( 'module\_name' string ) ? \\
+ 'export_code' ( constexpr + ) \\
+ ( ( 'in' target ( 'module_name' string ) ? \\
( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
;
@@ -1100,10 +1101,10 @@
'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
- 'code\_abort' ( const + )
+ 'code_abort' ( const + )
;
- 'code\_datatype' ( const + )
+ 'code_datatype' ( const + )
;
'code_inline' ( 'del' ) ?
@@ -1112,41 +1113,41 @@
'code_post' ( 'del' ) ?
;
- 'code\_thms' ( constexpr + ) ?
+ 'code_thms' ( constexpr + ) ?
;
- 'code\_deps' ( constexpr + ) ?
+ 'code_deps' ( constexpr + ) ?
;
- 'code\_const' (const + 'and') \\
+ 'code_const' (const + 'and') \\
( ( '(' target ( syntax ? + 'and' ) ')' ) + )
;
- 'code\_type' (typeconstructor + 'and') \\
+ 'code_type' (typeconstructor + 'and') \\
( ( '(' target ( syntax ? + 'and' ) ')' ) + )
;
- 'code\_class' (class + 'and') \\
+ 'code_class' (class + 'and') \\
( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
;
- 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
+ 'code_instance' (( typeconstructor '::' class ) + 'and') \\
( ( '(' target ( '-' ? + 'and' ) ')' ) + )
;
- 'code\_reserved' target ( string + )
+ 'code_reserved' target ( string + )
;
- 'code\_monad' const const target
+ 'code_monad' const const target
;
- 'code\_include' target ( string ( string | '-') )
+ 'code_include' target ( string ( string | '-') )
;
- 'code\_modulename' target ( ( string string ) + )
+ 'code_modulename' target ( ( string string ) + )
;
- 'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+ 'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
( 'functions' ( string + ) ) ? ( 'file' string ) ?
;
@@ -1280,7 +1281,7 @@
\end{matharray}
\begin{rail}
- ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
+ ( 'code_module' | 'code_library' ) modespec ? name ? \\
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
'contains' ( ( name '=' term ) + | term + )
;
@@ -1288,13 +1289,13 @@
modespec: '(' ( name * ) ')'
;
- 'consts\_code' (codespec +)
+ 'consts_code' (codespec +)
;
codespec: const template attachment ?
;
- 'types\_code' (tycodespec +)
+ 'types_code' (tycodespec +)
;
tycodespec: name template attachment ?
@@ -1325,7 +1326,7 @@
\end{matharray}
\begin{rail}
- ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
+ ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
;
decl: ((name ':')? term '(' 'overloaded' ')'?)
\end{rail}
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Oct 29 17:38:57 2010 +0200
@@ -31,7 +31,7 @@
;
'thm' modes? thmrefs
;
- ( 'prf' | 'full\_prf' ) modes? thmrefs?
+ ( 'prf' | 'full_prf' ) modes? thmrefs?
;
'pr' modes? nat?
;
@@ -364,9 +364,9 @@
\end{matharray}
\begin{rail}
- ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
+ ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
;
- ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
+ ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
;
'write' mode? (nameref structmixfix + 'and')
;
@@ -730,9 +730,9 @@
\begin{rail}
'nonterminals' (name +)
;
- ('syntax' | 'no\_syntax') mode? (constdecl +)
+ ('syntax' | 'no_syntax') mode? (constdecl +)
;
- ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+ ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
;
mode: ('(' ( name | 'output' | name 'output' ) ')')
@@ -786,8 +786,8 @@
\end{matharray}
\begin{rail}
- ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
- 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
+ ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
+ 'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
;
\end{rail}
--- a/doc-src/IsarRef/Thy/Misc.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Misc.thy Fri Oct 29 17:38:57 2010 +0200
@@ -21,19 +21,19 @@
\end{matharray}
\begin{rail}
- ('print\_theory' | 'print\_theorems') ('!'?)
+ ('print_theory' | 'print_theorems') ('!'?)
;
- 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
+ 'find_theorems' (('(' (nat)? ('with_dups')? ')')?) (thmcriterion *)
;
thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
'solves' | 'simp' ':' term | term)
;
- 'find\_consts' (constcriterion *)
+ 'find_consts' (constcriterion *)
;
constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
;
- 'thm\_deps' thmrefs
+ 'thm_deps' thmrefs
;
\end{rail}
@@ -143,7 +143,7 @@
\end{matharray}
\begin{rail}
- ('cd' | 'use\_thy') name
+ ('cd' | 'use_thy') name
;
\end{rail}
--- a/doc-src/IsarRef/Thy/Proof.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Fri Oct 29 17:38:57 2010 +0200
@@ -432,11 +432,11 @@
\begin{rail}
('lemma' | 'theorem' | 'corollary' |
- 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
+ 'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
;
('have' | 'show' | 'hence' | 'thus') goal
;
- 'print\_statement' modes? thmrefs
+ 'print_statement' modes? thmrefs
;
goal: (props + 'and')
@@ -834,7 +834,7 @@
\end{matharray}
\begin{rail}
- ( 'apply' | 'apply\_end' ) method
+ ( 'apply' | 'apply_end' ) method
;
'defer' nat?
;
@@ -896,7 +896,7 @@
\end{matharray}
\begin{rail}
- 'method\_setup' name '=' text text
+ 'method_setup' name '=' text text
;
\end{rail}
@@ -1190,9 +1190,9 @@
caseref: nameref attributes?
;
- 'case\_names' (name +)
+ 'case_names' (name +)
;
- 'case\_conclusion' name (name *)
+ 'case_conclusion' name (name *)
;
'params' ((name *) + 'and')
;
--- a/doc-src/IsarRef/Thy/Spec.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Fri Oct 29 17:38:57 2010 +0200
@@ -322,8 +322,8 @@
A locale instance consists of a reference to a locale and either
positional or named parameter instantiations. Identical
instantiations (that is, those that instante a parameter by itself)
- may be omitted. The notation `\_' enables to omit the instantiation
- for a parameter inside a positional instantiation.
+ may be omitted. The notation `@{text "_"}' enables to omit the
+ instantiation for a parameter inside a positional instantiation.
Terms in instantiations are from the context the locale expressions
is declared in. Local names may be added to this context with the
@@ -360,7 +360,7 @@
\begin{rail}
'locale' name ('=' locale)? 'begin'?
;
- 'print\_locale' '!'? nameref
+ 'print_locale' '!'? nameref
;
locale: contextelem+ | localeexpr ('+' (contextelem+))?
;
@@ -503,7 +503,7 @@
;
'interpret' localeexpr equations?
;
- 'print\_interps' nameref
+ 'print_interps' nameref
;
equations: 'where' (thmdecl? prop + 'and')
;
@@ -630,9 +630,9 @@
;
'instance' nameref ('<' | subseteq) nameref
;
- 'print\_classes'
+ 'print_classes'
;
- 'class\_deps'
+ 'class_deps'
;
superclassexpr: nameref | (nameref '+' superclassexpr)
@@ -840,9 +840,9 @@
\begin{rail}
'use' name
;
- ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
+ ('ML' | 'ML_prf' | 'ML_val' | 'ML_command' | 'setup' | 'local_setup') text
;
- 'attribute\_setup' name '=' text text
+ 'attribute_setup' name '=' text text
;
\end{rail}
@@ -930,7 +930,7 @@
;
'classrel' (nameref ('<' | subseteq) nameref + 'and')
;
- 'default\_sort' sort
+ 'default_sort' sort
;
\end{rail}
@@ -1176,7 +1176,7 @@
\end{matharray}
\begin{rail}
- ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
+ ( 'hide_class' | 'hide_type' | 'hide_const' | 'hide_fact' ) ('(open)')? (nameref + )
;
\end{rail}
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Fri Oct 29 17:38:57 2010 +0200
@@ -67,11 +67,11 @@
;
monos: ('monos' thmrefs)?
;
- condefs: ('con\_defs' thmrefs)?
+ condefs: ('con_defs' thmrefs)?
;
- typeintros: ('type\_intros' thmrefs)?
+ typeintros: ('type_intros' thmrefs)?
;
- typeelims: ('type\_elims' thmrefs)?
+ typeelims: ('type_elims' thmrefs)?
;
\end{rail}
@@ -126,7 +126,7 @@
\end{matharray}
\begin{rail}
- ('case\_tac' | 'induct\_tac') goalspec? name
+ ('case_tac' | 'induct_tac') goalspec? name
;
indcases (prop +)
;
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Oct 29 17:38:57 2010 +0200
@@ -105,7 +105,7 @@
\begin{rail}
('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
;
- ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+ ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
;
\end{rail}
@@ -216,10 +216,10 @@
'goals' options |
'subgoals' options |
'prf' options thmrefs |
- 'full\_prf' options thmrefs |
+ 'full_prf' options thmrefs |
'ML' options name |
- 'ML\_type' options name |
- 'ML\_struct' options name
+ 'ML_type' options name |
+ 'ML_struct' options name
;
options: '[' (option * ',') ']'
;
@@ -487,7 +487,7 @@
\end{matharray}
\begin{rail}
- ('display\_drafts' | 'print\_drafts') (name +)
+ ('display_drafts' | 'print_drafts') (name +)
;
\end{rail}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Fri Oct 29 17:38:57 2010 +0200
@@ -302,14 +302,14 @@
\end{matharray}
\begin{rail}
- ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
+ ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
( insts thmref | thmrefs )
;
- 'subgoal\_tac' goalspec? (prop +)
+ 'subgoal_tac' goalspec? (prop +)
;
- 'rename\_tac' goalspec? (name +)
+ 'rename_tac' goalspec? (name +)
;
- 'rotate\_tac' goalspec? int?
+ 'rotate_tac' goalspec? int?
;
('tactic' | 'raw_tactic') text
;
@@ -384,10 +384,10 @@
\indexouternonterm{simpmod}
\begin{rail}
- ('simp' | 'simp\_all') opt? (simpmod *)
+ ('simp' | 'simp_all') opt? (simpmod *)
;
- opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
+ opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
;
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
'split' (() | 'add' | 'del')) ':' thmrefs
@@ -490,7 +490,7 @@
\end{matharray}
\begin{rail}
- 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
+ 'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
;
'simproc' (('add' ':')? | 'del' ':') (name+)
@@ -538,7 +538,7 @@
'simplified' opt? thmrefs?
;
- opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
+ opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
;
\end{rail}
@@ -809,7 +809,7 @@
;
'atomize' ('(' 'full' ')')?
;
- 'rule\_format' ('(' 'noasm' ')')?
+ 'rule_format' ('(' 'noasm' ')')?
;
\end{rail}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 29 17:38:57 2010 +0200
@@ -93,7 +93,7 @@
\end{matharray}
\begin{rail}
- 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+ 'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
;
\end{rail}
@@ -364,7 +364,7 @@
\begin{rail}
'datatype' (dtspec + 'and')
;
- 'rep\_datatype' ('(' (name +) ')')? (term +)
+ 'rep_datatype' ('(' (name +) ')')? (term +)
;
dtspec: parname? typespec mixfix? '=' (cons + '|')
@@ -511,9 +511,9 @@
\begin{rail}
'relation' term
;
- 'lexicographic\_order' ( clasimpmod * )
+ 'lexicographic_order' ( clasimpmod * )
;
- 'size\_change' ( orders ( clasimpmod * ) )
+ 'size_change' ( orders ( clasimpmod * ) )
;
orders: ( 'max' | 'min' | 'ms' ) *
\end{rail}
@@ -642,7 +642,7 @@
;
hints: '(' 'hints' ( recdefmod * ) ')'
;
- recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
+ recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
;
tc: nameref ('(' nat ')')?
;
@@ -680,7 +680,7 @@
\end{matharray}
\begin{rail}
- ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
+ ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
;
\end{rail}%
\end{isamarkuptext}%
@@ -722,7 +722,7 @@
\end{matharray}
\begin{rail}
- ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
+ ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
('where' clauses)? ('monos' thmrefs)?
;
clauses: (thmdecl? prop + '|')
@@ -959,14 +959,28 @@
\begin{description}
- \item[size] specifies the maximum size of the search space for
- assignment values.
+ \item[\isa{size}] specifies the maximum size of the search space
+ for assignment values.
+
+ \item[\isa{iterations}] sets how many sets of assignments are
+ generated for each particular size.
+
+ \item[\isa{no{\isacharunderscore}assms}] specifies whether assumptions in
+ structured proofs should be ignored.
+
+ \item[\isa{timeout}] sets the time limit in seconds.
- \item[iterations] sets how many sets of assignments are
- generated for each particular size.
+ \item[\isa{default{\isacharunderscore}type}] sets the type(s) generally used to
+ instantiate type variables.
+
+ \item[\isa{report}] if set quickcheck reports how many tests
+ fulfilled the preconditions.
- \item[no\_assms] specifies whether assumptions in
- structured proofs should be ignored.
+ \item[\isa{quiet}] if not set quickcheck informs about the
+ current size for assignment values.
+
+ \item[\isa{expect}] can be used to check if the user's
+ expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
\end{description}
@@ -996,13 +1010,13 @@
\end{matharray}
\begin{rail}
- 'case\_tac' goalspec? term rule?
+ 'case_tac' goalspec? term rule?
;
- 'induct\_tac' goalspec? (insts * 'and') rule?
+ 'induct_tac' goalspec? (insts * 'and') rule?
;
- 'ind\_cases' (prop +) ('for' (name +)) ?
+ 'ind_cases' (prop +) ('for' (name +)) ?
;
- 'inductive\_cases' (thmdecl? (prop +) + 'and')
+ 'inductive_cases' (thmdecl? (prop +) + 'and')
;
rule: ('rule' ':' thmref)
@@ -1079,8 +1093,8 @@
\end{matharray}
\begin{rail}
- 'export\_code' ( constexpr + ) \\
- ( ( 'in' target ( 'module\_name' string ) ? \\
+ 'export_code' ( constexpr + ) \\
+ ( ( 'in' target ( 'module_name' string ) ? \\
( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
;
@@ -1102,10 +1116,10 @@
'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
- 'code\_abort' ( const + )
+ 'code_abort' ( const + )
;
- 'code\_datatype' ( const + )
+ 'code_datatype' ( const + )
;
'code_inline' ( 'del' ) ?
@@ -1114,41 +1128,41 @@
'code_post' ( 'del' ) ?
;
- 'code\_thms' ( constexpr + ) ?
+ 'code_thms' ( constexpr + ) ?
;
- 'code\_deps' ( constexpr + ) ?
+ 'code_deps' ( constexpr + ) ?
;
- 'code\_const' (const + 'and') \\
+ 'code_const' (const + 'and') \\
( ( '(' target ( syntax ? + 'and' ) ')' ) + )
;
- 'code\_type' (typeconstructor + 'and') \\
+ 'code_type' (typeconstructor + 'and') \\
( ( '(' target ( syntax ? + 'and' ) ')' ) + )
;
- 'code\_class' (class + 'and') \\
+ 'code_class' (class + 'and') \\
( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
;
- 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
+ 'code_instance' (( typeconstructor '::' class ) + 'and') \\
( ( '(' target ( '-' ? + 'and' ) ')' ) + )
;
- 'code\_reserved' target ( string + )
+ 'code_reserved' target ( string + )
;
- 'code\_monad' const const target
+ 'code_monad' const const target
;
- 'code\_include' target ( string ( string | '-') )
+ 'code_include' target ( string ( string | '-') )
;
- 'code\_modulename' target ( ( string string ) + )
+ 'code_modulename' target ( ( string string ) + )
;
- 'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+ 'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
( 'functions' ( string + ) ) ? ( 'file' string ) ?
;
@@ -1279,7 +1293,7 @@
\end{matharray}
\begin{rail}
- ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
+ ( 'code_module' | 'code_library' ) modespec ? name ? \\
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
'contains' ( ( name '=' term ) + | term + )
;
@@ -1287,13 +1301,13 @@
modespec: '(' ( name * ) ')'
;
- 'consts\_code' (codespec +)
+ 'consts_code' (codespec +)
;
codespec: const template attachment ?
;
- 'types\_code' (tycodespec +)
+ 'types_code' (tycodespec +)
;
tycodespec: name template attachment ?
@@ -1325,7 +1339,7 @@
\end{matharray}
\begin{rail}
- ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
+ ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
;
decl: ((name ':')? term '(' 'overloaded' ')'?)
\end{rail}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Oct 29 17:38:57 2010 +0200
@@ -53,7 +53,7 @@
;
'thm' modes? thmrefs
;
- ( 'prf' | 'full\_prf' ) modes? thmrefs?
+ ( 'prf' | 'full_prf' ) modes? thmrefs?
;
'pr' modes? nat?
;
@@ -387,9 +387,9 @@
\end{matharray}
\begin{rail}
- ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
+ ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
;
- ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
+ ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
;
'write' mode? (nameref structmixfix + 'and')
;
@@ -749,9 +749,9 @@
\begin{rail}
'nonterminals' (name +)
;
- ('syntax' | 'no\_syntax') mode? (constdecl +)
+ ('syntax' | 'no_syntax') mode? (constdecl +)
;
- ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+ ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
;
mode: ('(' ( name | 'output' | name 'output' ) ')')
@@ -806,8 +806,8 @@
\end{matharray}
\begin{rail}
- ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
- 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
+ ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
+ 'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
;
\end{rail}
--- a/doc-src/IsarRef/Thy/document/Misc.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex Fri Oct 29 17:38:57 2010 +0200
@@ -41,19 +41,19 @@
\end{matharray}
\begin{rail}
- ('print\_theory' | 'print\_theorems') ('!'?)
+ ('print_theory' | 'print_theorems') ('!'?)
;
- 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
+ 'find_theorems' (('(' (nat)? ('with_dups')? ')')?) (thmcriterion *)
;
thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
'solves' | 'simp' ':' term | term)
;
- 'find\_consts' (constcriterion *)
+ 'find_consts' (constcriterion *)
;
constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
;
- 'thm\_deps' thmrefs
+ 'thm_deps' thmrefs
;
\end{rail}
@@ -164,7 +164,7 @@
\end{matharray}
\begin{rail}
- ('cd' | 'use\_thy') name
+ ('cd' | 'use_thy') name
;
\end{rail}
--- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Oct 29 17:38:57 2010 +0200
@@ -453,11 +453,11 @@
\begin{rail}
('lemma' | 'theorem' | 'corollary' |
- 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
+ 'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
;
('have' | 'show' | 'hence' | 'thus') goal
;
- 'print\_statement' modes? thmrefs
+ 'print_statement' modes? thmrefs
;
goal: (props + 'and')
@@ -843,7 +843,7 @@
\end{matharray}
\begin{rail}
- ( 'apply' | 'apply\_end' ) method
+ ( 'apply' | 'apply_end' ) method
;
'defer' nat?
;
@@ -903,7 +903,7 @@
\end{matharray}
\begin{rail}
- 'method\_setup' name '=' text text
+ 'method_setup' name '=' text text
;
\end{rail}
@@ -1192,9 +1192,9 @@
caseref: nameref attributes?
;
- 'case\_names' (name +)
+ 'case_names' (name +)
;
- 'case\_conclusion' name (name *)
+ 'case_conclusion' name (name *)
;
'params' ((name *) + 'and')
;
--- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 17:38:57 2010 +0200
@@ -346,8 +346,8 @@
A locale instance consists of a reference to a locale and either
positional or named parameter instantiations. Identical
instantiations (that is, those that instante a parameter by itself)
- may be omitted. The notation `\_' enables to omit the instantiation
- for a parameter inside a positional instantiation.
+ may be omitted. The notation `\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}' enables to omit the
+ instantiation for a parameter inside a positional instantiation.
Terms in instantiations are from the context the locale expressions
is declared in. Local names may be added to this context with the
@@ -385,7 +385,7 @@
\begin{rail}
'locale' name ('=' locale)? 'begin'?
;
- 'print\_locale' '!'? nameref
+ 'print_locale' '!'? nameref
;
locale: contextelem+ | localeexpr ('+' (contextelem+))?
;
@@ -525,7 +525,7 @@
;
'interpret' localeexpr equations?
;
- 'print\_interps' nameref
+ 'print_interps' nameref
;
equations: 'where' (thmdecl? prop + 'and')
;
@@ -653,9 +653,9 @@
;
'instance' nameref ('<' | subseteq) nameref
;
- 'print\_classes'
+ 'print_classes'
;
- 'class\_deps'
+ 'class_deps'
;
superclassexpr: nameref | (nameref '+' superclassexpr)
@@ -862,9 +862,9 @@
\begin{rail}
'use' name
;
- ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
+ ('ML' | 'ML_prf' | 'ML_val' | 'ML_command' | 'setup' | 'local_setup') text
;
- 'attribute\_setup' name '=' text text
+ 'attribute_setup' name '=' text text
;
\end{rail}
@@ -966,7 +966,7 @@
;
'classrel' (nameref ('<' | subseteq) nameref + 'and')
;
- 'default\_sort' sort
+ 'default_sort' sort
;
\end{rail}
@@ -1218,7 +1218,7 @@
\end{matharray}
\begin{rail}
- ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
+ ( 'hide_class' | 'hide_type' | 'hide_const' | 'hide_fact' ) ('(open)')? (nameref + )
;
\end{rail}
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Fri Oct 29 17:38:57 2010 +0200
@@ -91,11 +91,11 @@
;
monos: ('monos' thmrefs)?
;
- condefs: ('con\_defs' thmrefs)?
+ condefs: ('con_defs' thmrefs)?
;
- typeintros: ('type\_intros' thmrefs)?
+ typeintros: ('type_intros' thmrefs)?
;
- typeelims: ('type\_elims' thmrefs)?
+ typeelims: ('type_elims' thmrefs)?
;
\end{rail}
@@ -153,7 +153,7 @@
\end{matharray}
\begin{rail}
- ('case\_tac' | 'induct\_tac') goalspec? name
+ ('case_tac' | 'induct_tac') goalspec? name
;
indcases (prop +)
;