NEWS
4 months ago ago system option "system_heaps" supersedes various command-line options for "system build mode";
5 months ago ago streamlined specification interfaces
5 months ago ago sligthly more interpunctation and qualification
5 months ago ago tuned whitespace
5 months ago ago updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
5 months ago ago clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
5 months ago ago Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
5 months ago ago Exponentiation by squaring, fast modular exponentiation
5 months ago ago More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
5 months ago ago NEWS;
5 months ago ago merged
5 months ago ago added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
5 months ago ago proper congruence rule for image operator
5 months ago ago NEWS;
5 months ago ago discontinued obsolete option "checkpoint";
5 months ago ago revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;
5 months ago ago changed precedence of big operators: now like any other function symbol
5 months ago ago prefer proper strings in OCaml
5 months ago ago more appropriate section
6 months ago ago slightly more conventional naming schema
6 months ago ago Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
6 months ago ago updated news
6 months ago ago more conventional syntax for code_stmts antiquotation
6 months ago ago self-contained code modules for Haskell
6 months ago ago tuned;
6 months ago ago information with hyperlink to "isabelle-export:";
6 months ago ago added action "isabelle-export-browser";
6 months ago ago optional code export as theory export
6 months ago ago tuned;
6 months ago ago more robust algorithm for eliminating Suc patterns
6 months ago ago support for isabelle update -u control_cartouches;
6 months ago ago tuned;
6 months ago ago support for "isabelle update -u mixfix_cartouches";
6 months ago ago NEWS;
6 months ago ago mixfix annotations may use cartouches;
6 months ago ago merged
6 months ago ago new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
6 months ago ago prefer naming convention from datatype package for strong congruence rules
6 months ago ago {* verbatim *} is explicit legacy feature;
7 months ago ago more ML antiquotations;
7 months ago ago more general command 'generate_file' for registered file types, notably Haskell;
7 months ago ago use Isabelle fonts for all GUI look-and-feels;
7 months ago ago use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
8 months ago ago Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
8 months ago ago added ML antiquotation @{master_dir};
8 months ago ago support for user-defined Isabelle/Scala command-line tools;
8 months ago ago NEWS;
8 months ago ago tuned whitespace;
8 months ago ago 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;
8 months ago ago NEWS;
8 months ago ago clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
8 months ago ago merged
8 months ago ago tuned example;
8 months ago ago added GHC.read_source: read Haskell source text with antiquotations;
8 months ago ago add reconstruction by veriT in method smt
8 months ago ago NEWS;
9 months ago ago tuned grammar
9 months ago ago tuned grammar
9 months ago ago uniform naming of strong congruence rules
9 months ago ago tuned;