NEWS
11 months ago desharna added lemmas relpowp_left_unique and relpow_left_unique
11 months ago desharna added lemmas relpowp_right_unique and relpow_right_unique
11 months ago wenzelm clarified default "isabelle build -j0 -H";
11 months ago desharna merged
11 months ago desharna added lemmas relpow_trans[trans] and relpowp_trans[trans]
11 months ago paulson the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
11 months ago paulson NEWS: corrected the definition of convexity of functions
11 months ago desharna added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult
12 months ago wenzelm update to llncs-2.23;
12 months ago haftmann consolidated lemma name
13 months ago haftmann compactified specification of type class parity
14 months ago wenzelm removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);
14 months ago wenzelm provide src/Tools/Demo as example for system component with Isabelle/Scala tool;
14 months ago wenzelm NEWS;
14 months ago desharna NEWS
14 months ago haftmann more specific name for type class
14 months ago wenzelm more NEWS;
14 months ago haftmann slightly less technical formulation of very specific type class
14 months ago haftmann explicit type class for discrete linordered semidoms
15 months ago Fabian Huch NEWS and CONTRIBUTORS;
15 months ago wenzelm update documentation on simproc_setup;
15 months ago wenzelm proper morphism;
15 months ago wenzelm simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
15 months ago wenzelm added ML antiquotation "simproc_setup";
15 months ago wenzelm more NEWS;
15 months ago wenzelm more NEWS;
15 months ago wenzelm tuned structure;
15 months ago wenzelm distinguish proper interrupts from Poly/ML RTS breakdown;
15 months ago desharna NEWS
16 months ago wenzelm more NEWS;
16 months ago wenzelm explicitly reject 'handle' with catch-all patterns;
17 months ago wenzelm tuned NEWS;
17 months ago wenzelm NEWS;
17 months ago wenzelm merged
17 months ago wenzelm minimal documentation for build cluster support;
17 months ago wenzelm clarified command arguments: optionally restrict to given theories (from theory loader);
17 months ago wenzelm added Isar command 'print_context_tracing';
17 months ago wenzelm back to post-release mode -- after fork point;
17 months ago wenzelm update to polyml-219e0a248f70, with more robust support for ARM64;
18 months ago wenzelm prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
18 months ago wenzelm tuned NEWS: emphasize "isabelle build" add-ons;
18 months ago wenzelm added option -A for AFP root, following "isabelle sync";
18 months ago wenzelm update for release;
18 months ago paulson X = trivial_topology rather than topspace X = {}
18 months ago paulson News update referring to Analysis
18 months ago wenzelm more NEWS;
18 months ago wenzelm more NEWS;
18 months ago wenzelm NEWS;
18 months ago wenzelm revert ineffective b04ac8a017b2: etc/settings of polyml components needs to be changed as well;
18 months ago wenzelm ML_system_apple=false for more stability;
18 months ago wenzelm update to stack-2.9.3 with support for arm64-linux;
18 months ago wenzelm clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
18 months ago wenzelm tuned;
18 months ago paulson NEWS tweak
19 months ago desharna add proof method "order" to command "try0"
19 months ago kleing optional description in Eisbach "method" command;
19 months ago blanchet disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice
19 months ago wenzelm updated for release;
19 months ago wenzelm tuned NEWS;
19 months ago wenzelm more realistic factor;
less more (0) -3000 -1000 -300 -100 -60 tip