| 2012-03-01 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| 2012-02-28 |
blanchet |
spelling
|
file |
diff |
annotate
|
| 2012-02-24 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| 2012-02-22 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-02-18 |
krauss |
NEWS
|
file |
diff |
annotate
|
| 2012-02-17 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| 2012-02-16 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
discontinued obsolete "prems" fact;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| 2012-02-14 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-02-04 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
| 2012-01-31 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2012-01-30 |
blanchet |
docs and news
|
file |
diff |
annotate
|
| 2012-01-30 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-01-19 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
| 2012-01-17 |
bulwahn |
refreshing NEWS
|
file |
diff |
annotate
|
| 2012-01-16 |
wenzelm |
position constraints for numerals enable PIDE markup;
|
file |
diff |
annotate
|
| 2012-01-10 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-01-09 |
wenzelm |
misc tuning and reformatting;
|
file |
diff |
annotate
|
| 2012-01-06 |
haftmann |
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
|
file |
diff |
annotate
|
| 2012-01-06 |
haftmann |
more explicit NEWS
|
file |
diff |
annotate
|
| 2012-01-06 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
|
file |
diff |
annotate
|
| 2012-01-05 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file |
diff |
annotate
|
| 2012-01-05 |
wenzelm |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
| 2011-12-29 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| 2011-12-28 |
huffman |
fix typos
|
file |
diff |
annotate
|
| 2011-12-28 |
huffman |
remove some duplicate lemmas
|
file |
diff |
annotate
|
| 2011-12-27 |
haftmann |
be explicit about Finite_Set.fold
|
file |
diff |
annotate
|
| 2011-12-26 |
haftmann |
NEWS: unavoidable fact renames
|
file |
diff |
annotate
|
| 2011-12-24 |
haftmann |
NEWS: `set` is now a proper type constructor
|
file |
diff |
annotate
|
| 2011-12-23 |
huffman |
remove redundant lemma word_sub_def
|
file |
diff |
annotate
|
| 2011-12-21 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-12-14 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-12-13 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| 2011-12-10 |
huffman |
prove class instances without extra lemmas
|
file |
diff |
annotate
|
| 2011-12-09 |
huffman |
remove redundant lemma word_diff_minus
|
file |
diff |
annotate
|
| 2011-12-09 |
noschinl |
more systematic lemma name
|
file |
diff |
annotate
|
| 2011-12-05 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-12-04 |
huffman |
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
|
file |
diff |
annotate
|
| 2011-12-01 |
blanchet |
added "minimize" option for more control over automatic minimization
|
file |
diff |
annotate
|
| 2011-12-01 |
blanchet |
renamed "slicing" to "slice"
|
file |
diff |
annotate
|
| 2011-12-01 |
wenzelm |
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
|
file |
diff |
annotate
|
| 2011-11-24 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| 2011-11-23 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| 2011-11-21 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2011-11-20 |
wenzelm |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
file |
diff |
annotate
|
| 2011-11-19 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2011-11-19 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
| 2011-11-17 |
huffman |
HOL-Word: removed more duplicate theorems
|
file |
diff |
annotate
|
| 2011-11-17 |
huffman |
HOL-Word: removed many duplicate theorems (see NEWS)
|
file |
diff |
annotate
|
| 2011-11-16 |
blanchet |
document "lam_trans" option
|
file |
diff |
annotate
|
| 2011-11-09 |
wenzelm |
sort assignment before simultaneous term_check, not isolated parse_term;
|
file |
diff |
annotate
|
| 2011-11-07 |
blanchet |
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
|
file |
diff |
annotate
|
| 2011-11-07 |
wenzelm |
clarified attribute "mono_set": pure declaration, proper export in ML;
|
file |
diff |
annotate
|
| 2011-11-07 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| 2011-10-29 |
wenzelm |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
file |
diff |
annotate
|
| 2011-10-28 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
file |
diff |
annotate
|
| 2011-10-21 |
bulwahn |
NEWS
|
file |
diff |
annotate
|