| Fri, 07 Oct 2016 17:58:36 +0200 |
fleury |
tuning multisets
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 10:45:21 +0200 |
eberlm |
Set_Permutations -> Multiset_Permutations in NEWS
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 10:31:34 +0200 |
wenzelm |
moved to proper release (cf. 4a72b37ac4b8);
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 10:23:50 +0200 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| Mon, 03 Oct 2016 14:34:31 +0200 |
haftmann |
option to report results of solve_direct as explicit warnings
|
file |
diff |
annotate
|
| Sun, 02 Oct 2016 17:05:48 +0200 |
wenzelm |
added isabelle_java cold-start executable;
|
file |
diff |
annotate
|
| Sun, 02 Oct 2016 12:29:18 +0200 |
wenzelm |
just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 23:05:25 +0200 |
wenzelm |
options for process policy, notably for multiprocessor machines;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 17:16:35 +0200 |
wenzelm |
clarified lfp/gfp statements and proofs;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 12:03:27 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 14:05:51 +0100 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 20:54:45 +0200 |
boehmes |
NEWS: new proof method "argo"
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:53 +0200 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 11:25:27 +0200 |
wenzelm |
discontinued raw symbols;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 00:12:17 +0200 |
wenzelm |
raw control symbols are superseded by Latex.embed_raw;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2016 22:43:06 +0200 |
wenzelm |
more general mixfix delimiters;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2016 14:51:58 +0200 |
eberlm |
NEWS: Normalized_Fraction.thy
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 23:14:34 +0200 |
kuncar |
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:07:39 +0200 |
fleury |
# after multiset intersection and union symbol
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 12:53:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 15:16:42 +0200 |
wenzelm |
clarified notation;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 16:33:24 +0200 |
traytel |
NEWS
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Wed, 14 Sep 2016 20:57:43 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2016 14:37:38 +0200 |
wenzelm |
discontinued global etc/abbrevs;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 17:32:09 +0200 |
blanchet |
NEWS
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 15:12:40 +0200 |
nipkow |
msetsum -> set_mset, msetprod -> prod_mset
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 18:18:57 +0200 |
wenzelm |
option "checkpoint" helps to fine-tune global heap space management;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 22:28:30 +0200 |
wenzelm |
unfold_abs_def is enabled by default;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:39:15 +0200 |
wenzelm |
clarified obscure facts;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
tuning multisets; more interpretations
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
add_mset constructor in multisets
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 10:48:06 +0200 |
blanchet |
added warning
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 16:12:55 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 14:19:27 +0200 |
wenzelm |
uniform ML and document antiquotations;
|
file |
diff |
annotate
|
| Thu, 11 Aug 2016 18:26:44 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Thu, 11 Aug 2016 07:36:58 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 15:42:52 +0200 |
nipkow |
"split add" -> "split".
|
file |
diff |
annotate
|
| Tue, 09 Aug 2016 12:30:31 +0200 |
eberlm |
Tuned primes
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
|
| Sat, 06 Aug 2016 18:14:59 +0200 |
wenzelm |
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 16:30:53 +0200 |
wenzelm |
Sidekick parser for isabelle-ml and sml mode;
|
file |
diff |
annotate
|
| Thu, 04 Aug 2016 21:25:16 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2016 11:45:09 +0200 |
wenzelm |
include 'begin' and 'end' structure in text folds;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 18:11:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 17:35:18 +0200 |
wenzelm |
support 'abbrevs' within theory header;
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 08:22:59 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Sun, 24 Jul 2016 16:48:39 +0200 |
haftmann |
text antiquotation for locales (similar to classes)
|
file |
diff |
annotate
|
| Wed, 27 Jul 2016 10:44:22 +0200 |
Manuel Eberl |
NEWS: Primes
|
file |
diff |
annotate
|
| Thu, 21 Jul 2016 10:52:27 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 22:36:10 +0200 |
wenzelm |
provide Pure.simp/simp_all, which only know about meta-equality;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 16:02:00 +0200 |
wenzelm |
completion templates for commands involving "begin ... end" blocks;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 11:44:11 +0200 |
wenzelm |
moved method "use" to Pure;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 14:52:09 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 13:51:38 +0200 |
fleury |
adding mset_map to the simp rules
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 00:38:33 +0200 |
wenzelm |
information about proof outline with cases (sendback);
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 15:19:16 +0200 |
wenzelm |
semantic indentation for unstructured proof scripts;
|
file |
diff |
annotate
|