| Wed, 20 Mar 2019 20:15:30 +0100 |
wenzelm |
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 21:17:40 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 16:55:06 +0100 |
wenzelm |
more specific keyword kinds;
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 19:06:40 +0100 |
haftmann |
include zarith in the default opam setup
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 15:16:45 +0000 |
haftmann |
migrated from Nums to Zarith as library for OCaml integer arithmetic
|
file |
diff |
annotate
|
| Tue, 12 Mar 2019 15:34:33 +0100 |
wenzelm |
updated to polyml-5.8 (official release);
|
file |
diff |
annotate
|
| Tue, 05 Mar 2019 07:00:21 +0000 |
haftmann |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
file |
diff |
annotate
|
| Fri, 01 Mar 2019 21:29:59 +0100 |
wenzelm |
system option "system_heaps" supersedes various command-line options for "system build mode";
|
file |
diff |
annotate
|
| Thu, 21 Feb 2019 09:15:07 +0000 |
haftmann |
streamlined specification interfaces
|
file |
diff |
annotate
|
| Thu, 21 Feb 2019 09:15:06 +0000 |
haftmann |
sligthly more interpunctation and qualification
|
file |
diff |
annotate
|
| Thu, 21 Feb 2019 09:15:06 +0000 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Wed, 20 Feb 2019 12:10:40 +0100 |
wenzelm |
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
|
file |
diff |
annotate
|
| Fri, 15 Feb 2019 17:00:21 +0100 |
wenzelm |
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 17:19:04 +0100 |
Manuel Eberl |
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 15:39:37 +0100 |
Manuel Eberl |
Exponentiation by squaring, fast modular exponentiation
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 12:16:03 +0100 |
Manuel Eberl |
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 22:53:35 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 21:59:30 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 17:18:15 +0100 |
wenzelm |
added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Wed, 30 Jan 2019 21:18:26 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 30 Jan 2019 13:25:33 +0100 |
wenzelm |
discontinued obsolete option "checkpoint";
|
file |
diff |
annotate
|
| Mon, 28 Jan 2019 20:32:09 +0100 |
wenzelm |
revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2019 16:29:11 +0100 |
nipkow |
changed precedence of big operators: now like any other function symbol
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 22:13:48 +0000 |
haftmann |
prefer proper strings in OCaml
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 10:04:32 +0100 |
haftmann |
more appropriate section
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 07:08:55 +0000 |
haftmann |
slightly more conventional naming schema
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 07:08:27 +0000 |
haftmann |
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 22:46:25 +0100 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Sun, 20 Jan 2019 17:14:35 +0000 |
haftmann |
more conventional syntax for code_stmts antiquotation
|
file |
diff |
annotate
|
| Sat, 19 Jan 2019 07:19:16 +0000 |
haftmann |
self-contained code modules for Haskell
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 17:56:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2019 20:25:41 +0100 |
wenzelm |
information with hyperlink to "isabelle-export:";
|
file |
diff |
annotate
|
| Sun, 13 Jan 2019 13:33:23 +0100 |
wenzelm |
added action "isabelle-export-browser";
|
file |
diff |
annotate
|
| Thu, 10 Jan 2019 12:07:08 +0000 |
haftmann |
optional code export as theory export
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 16:07:18 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 21:49:06 +0100 |
wenzelm |
support for isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 21:36:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 21:06:39 +0100 |
wenzelm |
support for "isabelle update -u mixfix_cartouches";
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 21:04:16 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 16:42:15 +0100 |
wenzelm |
mixfix annotations may use cartouches;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 18:33:19 +0100 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 17:04:53 +0100 |
Andreas Lochbihler |
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
|
file |
diff |
annotate
|
| Sun, 30 Dec 2018 10:34:56 +0000 |
haftmann |
prefer naming convention from datatype package for strong congruence rules
|
file |
diff |
annotate
|
| Wed, 26 Dec 2018 20:57:23 +0100 |
wenzelm |
{* verbatim *} is explicit legacy feature;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2018 11:43:48 +0100 |
wenzelm |
more ML antiquotations;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2018 23:43:10 +0100 |
wenzelm |
more general command 'generate_file' for registered file types, notably Haskell;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2018 14:46:00 +0100 |
wenzelm |
use Isabelle fonts for all GUI look-and-feels;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2018 18:56:44 +0100 |
wenzelm |
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2018 13:40:04 +0100 |
nipkow |
Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 19:39:38 +0100 |
wenzelm |
added ML antiquotation @{master_dir};
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 14:08:02 +0100 |
wenzelm |
support for user-defined Isabelle/Scala command-line tools;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:35:17 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 16:21:46 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 16:18:12 +0100 |
wenzelm |
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2018 20:30:10 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Tue, 30 Oct 2018 22:59:06 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 30 Oct 2018 22:08:36 +0100 |
wenzelm |
tuned example;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2018 22:05:30 +0100 |
wenzelm |
added GHC.read_source: read Haskell source text with antiquotations;
|
file |
diff |
annotate
|