NEWS
2 months ago wenzelm 2019-03-20 access OCaml tools and libraries via ISABELLE_OCAMLFIND; OPAM setup is optional: it requires odd development tools that are not available in default OS installations (e.g. make, m4);
2 months ago wenzelm 2019-03-14 merged
2 months ago wenzelm 2019-03-14 more specific keyword kinds;
2 months ago haftmann 2019-03-14 include zarith in the default opam setup
2 months ago haftmann 2019-03-10 migrated from Nums to Zarith as library for OCaml integer arithmetic
2 months ago wenzelm 2019-03-12 updated to polyml-5.8 (official release);
2 months ago haftmann 2019-03-05 avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
2 months ago wenzelm 2019-03-01 system option "system_heaps" supersedes various command-line options for "system build mode"; clarified "isabelle jedit" options -n, -s, -u;
2 months ago haftmann 2019-02-21 streamlined specification interfaces
2 months ago haftmann 2019-02-21 sligthly more interpunctation and qualification
2 months ago haftmann 2019-02-21 tuned whitespace
3 months ago wenzelm 2019-02-20 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
3 months ago wenzelm 2019-02-15 clarified 'export_files' in session ROOT: require explicit "isabelle build -e"; tuned messages;
3 months ago Manuel Eberl 2019-02-04 Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
3 months ago Manuel Eberl 2019-02-04 Exponentiation by squaring, fast modular exponentiation
3 months ago Manuel Eberl 2019-02-04 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
3 months ago wenzelm 2019-01-31 NEWS;
3 months ago wenzelm 2019-01-31 merged
3 months ago wenzelm 2019-01-31 added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
3 months ago haftmann 2019-01-31 proper congruence rule for image operator
3 months ago wenzelm 2019-01-30 NEWS;
3 months ago wenzelm 2019-01-30 discontinued obsolete option "checkpoint";
3 months ago wenzelm 2019-01-28 revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;
3 months ago nipkow 2019-01-28 changed precedence of big operators: now like any other function symbol
3 months ago haftmann 2019-01-25 prefer proper strings in OCaml
3 months ago haftmann 2019-01-24 more appropriate section
4 months ago haftmann 2019-01-21 slightly more conventional naming schema
4 months ago haftmann 2019-01-21 Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
4 months ago blanchet 2019-01-21 updated news
4 months ago haftmann 2019-01-20 more conventional syntax for code_stmts antiquotation
4 months ago haftmann 2019-01-19 self-contained code modules for Haskell
4 months ago wenzelm 2019-01-16 tuned;
4 months ago wenzelm 2019-01-13 information with hyperlink to "isabelle-export:";
4 months ago wenzelm 2019-01-13 added action "isabelle-export-browser";
4 months ago haftmann 2019-01-10 optional code export as theory export
4 months ago wenzelm 2019-01-06 tuned;
4 months ago wenzelm 2019-01-04 support for isabelle update -u control_cartouches;
4 months ago wenzelm 2019-01-03 tuned;
4 months ago wenzelm 2019-01-03 support for "isabelle update -u mixfix_cartouches";
4 months ago wenzelm 2019-01-03 NEWS;
4 months ago wenzelm 2019-01-03 mixfix annotations may use cartouches;
4 months ago Andreas Lochbihler 2019-01-01 merged
4 months ago Andreas Lochbihler 2019-01-01 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
4 months ago haftmann 2018-12-30 prefer naming convention from datatype package for strong congruence rules
4 months ago wenzelm 2018-12-26 {* verbatim *} is explicit legacy feature;
5 months ago wenzelm 2018-12-14 more ML antiquotations;
5 months ago wenzelm 2018-11-30 more general command 'generate_file' for registered file types, notably Haskell; discontinued 'generate_haskell_file', 'export_haskell_file'; eliminated generated sources: compile files in tmp dir;
5 months ago wenzelm 2018-11-30 use Isabelle fonts for all GUI look-and-feels;
5 months ago wenzelm 2018-11-24 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
6 months ago nipkow 2018-11-19 Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
6 months ago wenzelm 2018-11-10 added ML antiquotation @{master_dir};
6 months ago wenzelm 2018-11-10 support for user-defined Isabelle/Scala command-line tools; misc tuning and clarification;
6 months ago wenzelm 2018-11-08 NEWS;
6 months ago wenzelm 2018-11-08 tuned whitespace;
6 months ago wenzelm 2018-11-08 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;
6 months ago wenzelm 2018-11-03 NEWS;
6 months ago wenzelm 2018-10-31 clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
6 months ago wenzelm 2018-10-30 merged
6 months ago wenzelm 2018-10-30 tuned example;
6 months ago wenzelm 2018-10-30 added GHC.read_source: read Haskell source text with antiquotations; added "cartouche" antiquotation for ML string expressions as Haskell string literals;