NEWS
6 weeks ago haftmann 2019-03-10 migrated from Nums to Zarith as library for OCaml integer arithmetic
5 weeks ago wenzelm 2019-03-12 updated to polyml-5.8 (official release);
6 weeks ago haftmann 2019-03-05 avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
7 weeks 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
2 months ago wenzelm 2019-02-20 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
2 months ago wenzelm 2019-02-15 clarified 'export_files' in session ROOT: require explicit "isabelle build -e"; tuned messages;
2 months ago Manuel Eberl 2019-02-04 Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
2 months ago Manuel Eberl 2019-02-04 Exponentiation by squaring, fast modular exponentiation
2 months ago Manuel Eberl 2019-02-04 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
2 months ago wenzelm 2019-01-31 NEWS;
2 months ago wenzelm 2019-01-31 merged
2 months ago wenzelm 2019-01-31 added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
2 months ago haftmann 2019-01-31 proper congruence rule for image operator
2 months ago wenzelm 2019-01-30 NEWS;
2 months ago wenzelm 2019-01-30 discontinued obsolete option "checkpoint";
2 months ago wenzelm 2019-01-28 revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;
2 months ago nipkow 2019-01-28 changed precedence of big operators: now like any other function symbol
2 months ago haftmann 2019-01-25 prefer proper strings in OCaml
2 months ago haftmann 2019-01-24 more appropriate section
3 months ago haftmann 2019-01-21 slightly more conventional naming schema
3 months ago haftmann 2019-01-21 Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
3 months ago blanchet 2019-01-21 updated news
3 months ago haftmann 2019-01-20 more conventional syntax for code_stmts antiquotation
3 months ago haftmann 2019-01-19 self-contained code modules for Haskell
3 months ago wenzelm 2019-01-16 tuned;
3 months ago wenzelm 2019-01-13 information with hyperlink to "isabelle-export:";
3 months ago wenzelm 2019-01-13 added action "isabelle-export-browser";
3 months ago haftmann 2019-01-10 optional code export as theory export
3 months ago wenzelm 2019-01-06 tuned;
3 months ago wenzelm 2019-01-04 support for isabelle update -u control_cartouches;
3 months ago wenzelm 2019-01-03 tuned;
3 months ago wenzelm 2019-01-03 support for "isabelle update -u mixfix_cartouches";
3 months ago wenzelm 2019-01-03 NEWS;
3 months ago wenzelm 2019-01-03 mixfix annotations may use cartouches;
3 months ago Andreas Lochbihler 2019-01-01 merged
3 months ago Andreas Lochbihler 2019-01-01 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
3 months ago haftmann 2018-12-30 prefer naming convention from datatype package for strong congruence rules
3 months ago wenzelm 2018-12-26 {* verbatim *} is explicit legacy feature;
4 months ago wenzelm 2018-12-14 more ML antiquotations;
4 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;
4 months ago wenzelm 2018-11-30 use Isabelle fonts for all GUI look-and-feels;
4 months ago wenzelm 2018-11-24 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
5 months ago nipkow 2018-11-19 Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
5 months ago wenzelm 2018-11-10 added ML antiquotation @{master_dir};
5 months ago wenzelm 2018-11-10 support for user-defined Isabelle/Scala command-line tools; misc tuning and clarification;
5 months ago wenzelm 2018-11-08 NEWS;
5 months ago wenzelm 2018-11-08 tuned whitespace;
5 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;
5 months ago wenzelm 2018-11-03 NEWS;
5 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);
5 months ago wenzelm 2018-10-30 merged
5 months ago wenzelm 2018-10-30 tuned example;
5 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;
5 months ago fleury 2018-10-30 add reconstruction by veriT in method smt
5 months ago wenzelm 2018-10-25 NEWS;
5 months ago haftmann 2018-10-25 tuned grammar
6 months ago nipkow 2018-10-21 uniform naming of strong congruence rules