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