| 2016-10-24 |
eberlm |
Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
|
file |
diff |
annotate
|
| 2016-10-22 |
wenzelm |
regular user tool;
|
file |
diff |
annotate
|
| 2016-10-20 |
nipkow |
tuned
|
file |
diff |
annotate
|
| 2016-10-18 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2016-10-19 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2016-10-19 |
wenzelm |
added system option "profiling";
|
file |
diff |
annotate
|
| 2016-10-18 |
haftmann |
suitable logical type class for abs, sgn
|
file |
diff |
annotate
|
| 2016-10-17 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2016-10-17 |
wenzelm |
re-use "threads" for --gcthreads;
|
file |
diff |
annotate
|
| 2016-10-16 |
wenzelm |
isabelle build -N;
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
clarified theorem names
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| 2016-10-10 |
paulson |
invariance of domain
|
file |
diff |
annotate
|
| 2016-10-08 |
haftmann |
dedicated syntax for types with a length
|
file |
diff |
annotate
|
| 2016-10-08 |
fleury |
clarifying NEWS file
|
file |
diff |
annotate
|
| 2016-10-07 |
fleury |
tuning multisets
|
file |
diff |
annotate
|
| 2016-10-07 |
eberlm |
Set_Permutations -> Multiset_Permutations in NEWS
|
file |
diff |
annotate
|
| 2016-10-07 |
wenzelm |
moved to proper release (cf. 4a72b37ac4b8);
|
file |
diff |
annotate
|
| 2016-10-07 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2016-10-03 |
haftmann |
option to report results of solve_direct as explicit warnings
|
file |
diff |
annotate
|
| 2016-10-02 |
wenzelm |
added isabelle_java cold-start executable;
|
file |
diff |
annotate
|
| 2016-10-02 |
wenzelm |
just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
|
file |
diff |
annotate
|
| 2016-10-01 |
wenzelm |
options for process policy, notably for multiprocessor machines;
|
file |
diff |
annotate
|
| 2016-10-01 |
wenzelm |
clarified lfp/gfp statements and proofs;
|
file |
diff |
annotate
|
| 2016-10-01 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2016-09-30 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
| 2016-09-29 |
boehmes |
NEWS: new proof method "argo"
|
file |
diff |
annotate
|
| 2016-09-26 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| 2016-09-26 |
haftmann |
spelling
|
file |
diff |
annotate
|
| 2016-09-22 |
wenzelm |
discontinued raw symbols;
|
file |
diff |
annotate
|
| 2016-09-21 |
wenzelm |
raw control symbols are superseded by Latex.embed_raw;
|
file |
diff |
annotate
|
| 2016-09-21 |
wenzelm |
more general mixfix delimiters;
|
file |
diff |
annotate
|
| 2016-09-20 |
eberlm |
NEWS: Normalized_Fraction.thy
|
file |
diff |
annotate
|
| 2016-09-19 |
kuncar |
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
|
file |
diff |
annotate
|
| 2016-09-19 |
fleury |
# after multiset intersection and union symbol
|
file |
diff |
annotate
|
| 2016-09-19 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| 2016-09-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-09-18 |
wenzelm |
clarified notation;
|
file |
diff |
annotate
|
| 2016-09-16 |
traytel |
NEWS
|
file |
diff |
annotate
|
| 2016-09-15 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| 2016-09-14 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2016-09-14 |
wenzelm |
discontinued global etc/abbrevs;
|
file |
diff |
annotate
|
| 2016-09-12 |
blanchet |
NEWS
|
file |
diff |
annotate
|
| 2016-09-09 |
nipkow |
msetsum -> set_mset, msetprod -> prod_mset
|
file |
diff |
annotate
|
| 2016-09-08 |
wenzelm |
option "checkpoint" helps to fine-tune global heap space management;
|
file |
diff |
annotate
|
| 2016-09-07 |
wenzelm |
unfold_abs_def is enabled by default;
|
file |
diff |
annotate
|
| 2016-09-05 |
wenzelm |
clarified obscure facts;
|
file |
diff |
annotate
|
| 2016-09-05 |
fleury |
tuning multisets; more interpretations
|
file |
diff |
annotate
|
| 2016-09-05 |
fleury |
add_mset constructor in multisets
|
file |
diff |
annotate
|
| 2016-09-05 |
blanchet |
added warning
|
file |
diff |
annotate
|
| 2016-09-01 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2016-08-14 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| 2016-08-12 |
wenzelm |
uniform ML and document antiquotations;
|
file |
diff |
annotate
|
| 2016-08-11 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| 2016-08-11 |
nipkow |
tuned
|
file |
diff |
annotate
|
| 2016-08-10 |
nipkow |
"split add" -> "split".
|
file |
diff |
annotate
|
| 2016-08-09 |
eberlm |
Tuned primes
|
file |
diff |
annotate
|