Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-768
+768
+1000
+3000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
clarified signature;
2020-10-12, by wenzelm
clarified Executable.libraries_closure;
2020-10-12, by wenzelm
dedicated module for toplevel target handling
2020-10-12, by haftmann
avoid _cmd suffix where no Isar command is involved
2020-10-12, by haftmann
replaced combinators by more conventional nesting pattern
2020-10-12, by haftmann
consolidated names and operations
2020-10-12, by haftmann
centralized case distinction for beginning and ending nested targets in one place
2020-10-12, by haftmann
support for platform-specific executables;
2020-10-11, by wenzelm
merged
2020-10-11, by paulson
merged
2020-10-11, by paulson
tidying and removal of legacy name
2020-10-11, by paulson
tuned whitespace;
2020-10-11, by wenzelm
more robust: ignore existing gmp installation, but let veriT incorporate extern/gmp;
2020-10-11, by wenzelm
clarified signature;
2020-10-11, by wenzelm
presumably redundant (absent in Windows/Cygwin download);
2020-10-11, by wenzelm
tuned messages;
2020-10-11, by wenzelm
build Isabelle veriT component from official download;
2020-10-11, by wenzelm
tuned;
2020-10-11, by wenzelm
tuned messages;
2020-10-11, by wenzelm
direct exit to theory when ending nested target on theory target
2020-10-10, by haftmann
tuned
2020-10-10, by haftmann
consolidated terminology
2020-10-10, by haftmann
avoid baroque export
2020-10-10, by haftmann
clarified message;
2020-10-10, by wenzelm
tuned signature;
2020-10-10, by wenzelm
clarified options;
2020-10-10, by wenzelm
more explicit MinGW context;
2020-10-10, by wenzelm
clarified signature: allow complex bash script;
2020-10-10, by wenzelm
clarified signature;
2020-10-10, by wenzelm
more standard path output (despite platform_path from d55eb82ae77b);
2020-10-10, by wenzelm
clarified errors;
2020-10-10, by wenzelm
tuned signature;
2020-10-10, by wenzelm
more explicit MinGW context;
2020-10-10, by wenzelm
more libs for build_csdp;
2020-10-10, by wenzelm
support for MSYS2/MinGW64 on Windows;
2020-10-10, by wenzelm
tuned --- according to instructions on Website;
2020-10-10, by wenzelm
updated to csdp-6.1.1, with support for arm64-linux;
2020-10-10, by wenzelm
proper support for x86_64-windows via msys/mingw64;
2020-10-10, by wenzelm
more standard build from sources;
2020-10-10, by wenzelm
tuned message;
2020-10-10, by wenzelm
component csdp-6.2.0 for testing: example #2 in theory HOL-ex.SOS fails with return code 206;
2020-10-09, by wenzelm
build Isabelle CSDP component from official downloads;
2020-10-09, by wenzelm
rebuild component following current "isabelle build_e" and Admin/PLATFORMS;
2020-10-09, by wenzelm
proper support for Windows/Cygwin;
2020-10-09, by wenzelm
build Isabelle SPASS component from unofficial download;
2020-10-09, by wenzelm
tuned;
2020-10-09, by wenzelm
clarified according to Isabelle_System.download;
2020-10-09, by wenzelm
misc tuning;
2020-10-09, by wenzelm
rebuild component following current "isabelle build_e" and Admin/PLATFORMS;
2020-10-09, by wenzelm
discontinued unused eproof_ram (actually absent in version 2.5);
2020-10-09, by wenzelm
discontinued obsolete runepar.pl (see 4a3169d8885c);
2020-10-09, by wenzelm
tuned mirabelle documentation
2020-10-08, by blanchet
removed support for obsolete prover SNARK and underperforming prover E-Par
2020-10-08, by blanchet
removed spurious documentation item
2020-10-08, by blanchet
removed obsolete unmaintained experimental prover Pirate
2020-10-08, by blanchet
tune filename
2020-10-08, by desharna
drop obsolete ad hoc support for Satallax isar proof reconstruction
2020-10-08, by desharna
recognize THF proofs properly
2020-10-08, by desharna
factored out bit comprehension
2020-10-08, by haftmann
Fix formatting of default value in help message of "build_e" component.
2020-10-08, by desharna
tuned signature;
2020-10-07, by wenzelm
updated user + host;
2020-10-07, by wenzelm
updated URL;
2020-10-07, by wenzelm
clarified multicore options;
2020-10-07, by wenzelm
discontinued old machines;
2020-10-07, by wenzelm
updated tests for macOS 10.14 Mojave;
2020-10-07, by wenzelm
Aded Queues
2020-10-07, by nipkow
consolidated for the sake of documentation
2020-10-07, by haftmann
tuned;
2020-10-07, by wenzelm
merged
2020-10-06, by paulson
Simplified some proofs
2020-10-06, by paulson
added lemmas; internalized defn in class
2020-10-06, by nipkow
merged
2020-10-05, by paulson
still not quite fixed...
2020-10-05, by paulson
A few more reversions
2020-10-05, by paulson
reversion to the explicit existential quantifier
2020-10-05, by paulson
more tidying of messy proofs
2020-10-05, by paulson
clarified signature;
2020-10-05, by wenzelm
clarified signature;
2020-10-05, by wenzelm
clarified signature;
2020-10-05, by wenzelm
clarified signature;
2020-10-05, by wenzelm
merged
2020-10-03, by paulson
merged
2020-10-03, by paulson
de-applying
2020-10-03, by paulson
clarified arm64-linux base line: prefer Pi OS, which is based on slightly older Debian;
2020-10-03, by wenzelm
detect/guess arm32 platform (unsupported);
2020-10-03, by wenzelm
build component according to "isabelle build_e -V 2.5" (inactive);
2020-10-03, by wenzelm
updated component according to "isabelle build_e -V 2.0";
2020-10-03, by wenzelm
proper usage;
2020-10-03, by wenzelm
clarified;
2020-10-03, by wenzelm
merged
2020-10-02, by wenzelm
clarified installed files;
2020-10-02, by wenzelm
build Isabelle E prover component from official downloads;
2020-10-02, by wenzelm
clarified signature;
2020-10-02, by wenzelm
updated for coming release;
2020-10-02, by wenzelm
updated to current cygwin-20201002, after 3.1.7-1 from 24-Aug-2020;
2020-10-02, by wenzelm
clarified platforms;
2020-10-02, by wenzelm
updated to opam-2.0.7;
2020-10-02, by wenzelm
merged
2020-10-02, by paulson
fixed a bunch of ugly proofs
2020-10-02, by paulson
Add more tacing to sledgehammer_isar_trace
2020-10-02, by desharna
support arm64-linux Poly/ML (slow bytecode interpreter only);
2020-10-01, by wenzelm
purge arm64-linux --- no build_release support yet;
2020-10-01, by wenzelm
more systematic platform support, including arm64-linux;
2020-10-01, by wenzelm
tuned according to hints by IntelliJ IDEA;
2020-10-01, by wenzelm
updated certificates to make it work again after recent changes to smt/z3 setup;
2020-09-30, by wenzelm
clarified signature;
2020-09-30, by wenzelm
merged
2020-09-30, by wenzelm
updated to sqlite-jdbc-3.32.3.2;
2020-09-30, by wenzelm
build Isabelle sqlite-jdbc component from official download;
2020-09-30, by wenzelm
support arm64-linux;
2020-09-30, by wenzelm
detect arm64-linux platform;
2020-09-30, by wenzelm
Effectively disable timeout for smt method/tactic
2020-09-30, by desharna
[mirabelle] add initial documentation in Sledgehammer's doc
2020-09-08, by desharna
clarified names;
2020-09-29, by wenzelm
clarified signature;
2020-09-29, by wenzelm
tuned signature;
2020-09-29, by wenzelm
formal platform information, notably for ssh;
2020-09-29, by wenzelm
clarified message;
2020-09-29, by wenzelm
more robust executor policy after shutdown;
2020-09-29, by wenzelm
clarified message;
2020-09-29, by wenzelm
clarified names;
2020-09-29, by wenzelm
more reactive kodkod execution: avoid confusion about timeout/deadline;
2020-09-29, by wenzelm
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
2020-09-29, by wenzelm
clarified default (see also 0c7a74a1c6d9);
2020-09-29, by wenzelm
tuned;
2020-09-29, by wenzelm
obsolete --- Java is always present via component;
2020-09-29, by wenzelm
obsolete --- KODKODI is always present via component;
2020-09-29, by wenzelm
obsolete --- ML module Nitpick resides within theory Nitpick (see also 7b8c366e34a2, 1fba360b5443);
2020-09-29, by wenzelm
merged
2020-09-29, by paulson
merged
2020-09-28, by paulson
de-applying
2020-09-28, by paulson
some support for document preparation in Isabelle/Scala;
2020-09-28, by wenzelm
unused (see 7b318273a4aa);
2020-09-28, by wenzelm
unused (see 564012e31db1);
2020-09-28, by wenzelm
more standard and more robust, following hints on the Net;
2020-09-28, by wenzelm
obsolete, T1 fonts are fine in lualatex (see also cc71f01f9fde);
2020-09-28, by wenzelm
prefer old-fashioned {\ss} to prevent problems with encoding in lualatex;
2020-09-28, by wenzelm
proper Windows 32bit platform;
2020-09-28, by wenzelm
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
2020-09-28, by wenzelm
suppress ligatures more robustly, notably for lualatex;
2020-09-27, by wenzelm
ISABELLE_PDFLATEX is now lualatex;
2020-09-27, by wenzelm
added lemma
2020-09-26, by nipkow
less bulky session stack;
2020-09-26, by wenzelm
clarified document export;
2020-09-26, by wenzelm
tuned signature;
2020-09-26, by wenzelm
discontinued obsolete DVI document format and related settings/tools;
2020-09-26, by wenzelm
clarified errors;
2020-09-26, by wenzelm
tuned signature;
2020-09-26, by wenzelm
tuned;
2020-09-26, by wenzelm
merged
2020-09-25, by paulson
reverted the substitution here
2020-09-25, by paulson
merged
2020-09-25, by paulson
fixed some remarkably ugly proofs
2020-09-25, by paulson
de-applying and tidying
2020-09-25, by paulson
follow Phabricator update 2020 Week 37;
2020-09-25, by wenzelm
clarified defaults for nitpick;
2020-09-25, by wenzelm
tuned nitpick message: more like quickcheck;
2020-09-25, by wenzelm
clarified;
2020-09-25, by wenzelm
evaluate Scala via running Isabelle/Scala;
2020-09-25, by wenzelm
more robust: avoid spurious line breaks that might confuse the scala interpreter;
2020-09-25, by wenzelm
clarified signature: proper eval/print via interpret;
2020-09-25, by wenzelm
clarified name;
2020-09-25, by wenzelm
factored out typedef material
2020-09-25, by haftmann
tuned;
2020-09-24, by wenzelm
tuned;
2020-09-24, by wenzelm
tuned;
2020-09-24, by wenzelm
proper platform_path for Windows;
2020-09-24, by wenzelm
evaluate PolyML via running Isabelle/ML;
2020-09-24, by wenzelm
output via file instead of stdout;
2020-09-24, by wenzelm
proper context;
2020-09-24, by wenzelm
clarified signature;
2020-09-24, by wenzelm
tuned signature;
2020-09-24, by wenzelm
tuned
2020-09-24, by nipkow
more thorough treatment of division, particularly signed division on int and word
2020-09-23, by haftmann
canonical enum instance for word
2020-09-23, by haftmann
merged
2020-09-20, by wenzelm
clarified signature;
2020-09-20, by wenzelm
proper ml_source: avoid duplicate Bash.string;
2020-09-20, by wenzelm
misc tuning and clarification: prefer functions over data;
2020-09-20, by wenzelm
tuned;
2020-09-20, by wenzelm
misc tuning and clarification;
2020-09-20, by wenzelm
tuned messages;
2020-09-20, by wenzelm
tuned;
2020-09-20, by wenzelm
merged
2020-09-20, by paulson
de-applying and simplifying
2020-09-20, by paulson
tuned
2020-09-18, by nipkow
removal of needless premises
2020-09-18, by paulson
merged
2020-09-17, by paulson
de-applying
2020-09-17, by paulson
dropped junk
2020-09-17, by haftmann
typo
2020-09-17, by haftmann
NEWS and CONTRIBUTORS
2020-09-17, by haftmann
integrated generic conversions into word corpse
2020-09-17, by haftmann
more lemmas
2020-09-17, by haftmann
added lemma
2020-09-15, by nipkow
de-applying
2020-09-13, by paulson
merged
2020-09-11, by paulson
merged
2020-09-11, by paulson
cleaned up some messy proofs
2020-09-11, by paulson
prefer current mathpartir.sty from underlying TeX distribution;
2020-09-11, by wenzelm
more checks;
2020-09-11, by wenzelm
more uniform color --- avoid odd transparency on Windows (due to jEdit default #666699a);
2020-09-11, by wenzelm
updated documentation;
2020-09-11, by wenzelm
tuned documentation;
2020-09-11, by wenzelm
clarified modules;
2020-09-10, by wenzelm
more uniform JVM vs. ML status widget;
2020-09-10, by wenzelm
clarified modules;
2020-09-10, by wenzelm
update to official jedit-5.6.0;
2020-09-08, by wenzelm
merged
2020-09-08, by paulson
tidying and de-applying
2020-09-08, by paulson
restructured
2020-09-08, by haftmann
tuned theory structure
2020-09-07, by haftmann
more on conversions
2020-09-07, by haftmann
generalized signed_take_bit
2020-09-05, by haftmann
more on conversions
2020-09-05, by haftmann
generalized
2020-09-05, by haftmann
a bit of tidying
2020-09-04, by paulson
merged
2020-09-01, by paulson
de-applying
2020-09-01, by paulson
discontinue export_document --- always enabled (reverting f0f83ce0badd);
2020-09-01, by wenzelm
unused (see also 7b318273a4aa);
2020-09-01, by wenzelm
tuned proofs;
2020-09-01, by wenzelm
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
2020-08-31, by wenzelm
a new lemma
2020-08-31, by paulson
more informative bibtex errors;
2020-08-31, by wenzelm
merged
2020-08-30, by paulson
minor tidying, also s->S and t->T
2020-08-30, by paulson
more on conversions
2020-08-30, by haftmann
merged
2020-08-29, by paulson
quite a bit of tidying
2020-08-29, by paulson
more robust interpretation of data;
2020-08-28, by wenzelm
merged
2020-08-28, by paulson
small quantifier fixes
2020-08-28, by paulson
just a bit of streamlining
2020-08-27, by paulson
but not the [cong] rule
2020-08-27, by paulson
tidying up some theorem statements
2020-08-27, by paulson
initial Kodkod.warmup: preloading and basic integrity test;
2020-08-27, by wenzelm
strict init of protocol handlers;
2020-08-27, by wenzelm
clarified treatment of add-on prover_options;
2020-08-27, by wenzelm
clarified signature;
2020-08-27, by wenzelm
clarified modules;
2020-08-27, by wenzelm
tuned;
2020-08-27, by wenzelm
clarified signature;
2020-08-27, by wenzelm
tiny tidy-up of proofs
2020-08-26, by paulson
updated to scala-2.12.12;
2020-08-25, by wenzelm
updated to polyml-test-a3cfdf648da: performance improvements for GC statistics;
2020-08-25, by wenzelm
NEWS;
2020-08-25, by wenzelm
test HOL-Nitpick_Examples with Isabelle/Scala instead of external process: much faster;
2020-08-25, by wenzelm
updated to kodkodi-1.5.6: more robust treatment of interrupt;
2020-08-25, by wenzelm
removed pointless version checks: Isabelle component integration does the job already;
2020-08-25, by wenzelm
more robust treatment of execution with interrupts;
2020-08-25, by wenzelm
suppress odd warning for context.exit();
2020-08-24, by wenzelm
more explicit treatment of interrupt;
2020-08-24, by wenzelm
tuned;
2020-08-24, by wenzelm
more flexible default for max_threads;
2020-08-24, by wenzelm
proper default for max_threads;
2020-08-24, by wenzelm
a proof of concept for generic conversions
2020-08-24, by haftmann
proper name (amending 742d94015918);
2020-08-22, by wenzelm
invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
2020-08-22, by wenzelm
avoid odd PIDE markup, notably in kokodi input;
2020-08-22, by wenzelm
clarified names;
2020-08-22, by wenzelm
clarified signature;
2020-08-22, by wenzelm
clarified signature;
2020-08-22, by wenzelm
proper treatment of timeout: <= 0 means already timed out, but for $KODKODI/bin/kodkodi it would mean NO timeout;
2020-08-22, by wenzelm
proper treatment of absolute deadline vs. relative timeout;
2020-08-22, by wenzelm
clarified session: no parent image for minor theory imports;
2020-08-22, by wenzelm
removed obsolete created_temp_dir: ISABELLE_TMP is always present for the running Isabelle/ML process;
2020-08-22, by wenzelm
more lemmas
2020-08-21, by haftmann
proper syntax declaration
2020-08-21, by haftmann
merged
2020-08-21, by paulson
reversing all the lex crap
2020-08-21, by paulson
tuned;
2020-08-20, by wenzelm
merged
2020-08-20, by wenzelm
preload library;
2020-08-20, by wenzelm
update to kodkodi-1.5.4-1;
2020-08-20, by wenzelm
clarified signature;
2020-08-20, by wenzelm
more realistic kodkod invocation, imitating command-line tool;
2020-08-19, by wenzelm
update to kodkodi-1.5.4;
2020-08-19, by wenzelm
rudiments of Scala interface for Kodkod;
2020-08-18, by wenzelm
updated to kodkodi-1.5.3: include KODKODI_CLASSPATH for Isabelle/Scala;
2020-08-18, by wenzelm
basic integration of Zipperposition 2.0
2020-08-20, by blanchet
tuned Mirabelle comments
2020-08-20, by blanchet
two more lex fixes
2020-08-20, by paulson
more lex fixes
2020-08-19, by paulson
Another go with lex: now lexordp back in class ord
2020-08-19, by paulson
List_Lexorder finally working
2020-08-18, by paulson
lexicographic ordering: new simp setup to prioritise the simpler "less_than" case
2020-08-18, by paulson
merged
2020-08-18, by paulson
fixed for new lex-order. And the effing indentation!
2020-08-18, by paulson
merged
2020-08-17, by paulson
S Holub's proposed generalisation of the lexicographic product of two orderings
2020-08-17, by paulson
allow user-defined server commands via isabelle_scala_service;
2020-08-17, by wenzelm
more systematic support for special directories;
2020-08-17, by wenzelm
proper init of cumulative settings;
2020-08-17, by wenzelm
upgrade phabricator: Promote 2020 Week 31 + subsequent change;
2020-08-16, by wenzelm
clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
2020-08-16, by wenzelm
proper protocol init (amending 065dcd80293e);
2020-08-15, by wenzelm
clarified names;
2020-08-15, by wenzelm
provide protocol handlers via isabelle_system_service;
2020-08-15, by wenzelm
prefer formal name;
2020-08-15, by wenzelm
clarified signature;
2020-08-14, by wenzelm
misc tuning;
2020-08-14, by wenzelm
clarified demo functions;
2020-08-14, by wenzelm
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
2020-08-14, by wenzelm
more documentation;
2020-08-13, by wenzelm
support JVM runtime statistics;
2020-08-13, by wenzelm
clarified worker threads;
2020-08-13, by wenzelm
misc tuning, based on hints by IntelliJ IDEA;
2020-08-13, by wenzelm
clarified GUI;
2020-08-13, by wenzelm
tuned GUI;
2020-08-13, by wenzelm
tuned GUI;
2020-08-13, by wenzelm
clarified order for GUI;
2020-08-13, by wenzelm
tuned;
2020-08-13, by wenzelm
clarified GUI;
2020-08-13, by wenzelm
show GC progress as "ML cleanup";
2020-08-12, by wenzelm
ML status widget similar to org.gjt.sp.jedit.gui.statusbar.MemoryStatusWidgetFactory;
2020-08-12, by wenzelm
support for Poly/ML memory status;
2020-08-12, by wenzelm
clarified signature;
2020-08-12, by wenzelm
removed pointless option "ML_statistics": always enabled;
2020-08-12, by wenzelm
removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);
2020-08-12, by wenzelm
support for GC state;
2020-08-12, by wenzelm
updated to polyml-test-f54aa41240d0;
2020-08-11, by wenzelm
back to polyml-5.8.1 due to ML compiler crash in HOL-Codegenerator_Test;
2020-08-11, by wenzelm
updated to polyml-test-159dc81efc3b;
2020-08-11, by wenzelm
dedicated symbols for code generation, to pave way for generic conversions from and to word
2020-08-10, by haftmann
consolidated names
2020-08-10, by haftmann
reduced prominence od theory Bits_Int
2020-08-10, by haftmann
one last lemma about Total and Restr
2020-08-09, by paulson
adjustments for fewer WO assumptions
2020-08-09, by paulson
elimination of some needless assumptions
2020-08-09, by paulson
merged
2020-08-09, by paulson
iso lemmas
2020-08-08, by paulson
tuned
2020-08-08, by nipkow
tuned
2020-08-08, by nipkow
NEWS;
2020-08-07, by wenzelm
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
2020-08-07, by wenzelm
adapted to 7b318273a4aa;
2020-08-07, by wenzelm
cache props;
2020-08-07, by wenzelm
clarified names;
2020-08-07, by wenzelm
more thorough protocol_handlers.exit, like file_formats.stop_session;
2020-08-07, by wenzelm
tuned names;
2020-08-07, by wenzelm
temporary workaround for 100% CPU usage in OS.Process.sleep;
2020-08-07, by wenzelm
ML statistics via external process: allows monitoring RTS while ML program sleeps;
2020-08-07, by wenzelm
clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt in varying ML contexts;
2020-08-07, by wenzelm
avoid failure of "isabelle build -o skip_proofs";
2020-08-07, by wenzelm
merged
2020-08-06, by wenzelm
recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a);
2020-08-06, by wenzelm
more compact command_timings, as in former batch-build;
2020-08-06, by wenzelm
unused;
2020-08-06, by wenzelm
unused --- superseded by PIDE messages;
2020-08-06, by wenzelm
more thorough cleanup, e.g. before ML_Heap.save;
2020-08-06, by wenzelm
discontinued old batch-build functionality;
2020-08-06, by wenzelm
tailored towards remaining essence
2020-08-06, by haftmann
merged
2020-08-06, by nipkow
tuned
2020-08-06, by nipkow
added theory Tree23_of_List
2020-08-06, by nipkow
more robust treatment of thm_names, with strict check after all theories are loaded;
2020-08-06, by wenzelm
a few more lemmas
2020-08-06, by paulson
merged
2020-08-05, by paulson
lemmas about sets and the enumerate operator
2020-08-05, by paulson
yet another little lemma
2020-08-05, by paulson
merged
2020-08-05, by paulson
merged
2020-08-04, by paulson
merged
2020-08-03, by paulson
strengthened a lemma
2020-07-31, by paulson
A new lemma about abstract Sum / Prod
2020-07-31, by paulson
separation of reversed bit lists from other material
2020-08-05, by haftmann
merged
2020-08-05, by wenzelm
avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node;
2020-08-05, by wenzelm
more robust: insist in finished future;
2020-08-05, by wenzelm
unused;
2020-08-05, by wenzelm
further refinement of code equations for mask operation
2020-08-05, by haftmann
uniform mask operation
2020-08-04, by haftmann
clearer separation of pre-word bit list material
2020-08-04, by haftmann
added lemma
2020-08-03, by nipkow
more consequent transferability
2020-08-01, by haftmann
more robust scheduler shutdown, notably for spurious crashes;
2020-07-29, by wenzelm
unclear why I ever asked for type tree2
2020-07-27, by nipkow
enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it;
2020-07-26, by wenzelm
proper pretty printing for latex output, notably for pide_session=true (default);
2020-07-26, by wenzelm
clarified name to avoid duplication (no distinction of data on host = lrzcloud2);
2020-07-25, by wenzelm
clarified names;
2020-07-25, by wenzelm
more errors;
2020-07-25, by wenzelm
follow Phabricator update 2020 Week 27;
2020-07-24, by wenzelm
tuned;
2020-07-24, by wenzelm
unused;
2020-07-24, by wenzelm
clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);
2020-07-24, by wenzelm
clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
2020-07-24, by wenzelm
clarified signature;
2020-07-23, by wenzelm
clarified order --- proper sorting of requirements;
2020-07-23, by wenzelm
obsolete (see 9cde8c4ea5a5);
2020-07-23, by wenzelm
tuned --- based on hints by IntelliJ;
2020-07-21, by wenzelm
tuned signature;
2020-07-21, by wenzelm
updated to polyml-5.8.1 (official release);
2020-07-21, by wenzelm
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
2020-07-20, by wenzelm
clarified -- avoid non-standard extend/merge;
2020-07-17, by wenzelm
tuned -- avoid non-standard extend;
2020-07-17, by wenzelm
clarified -- avoid non-standard extend/merge;
2020-07-17, by wenzelm
proper session imports;
2020-07-17, by wenzelm
clarified -- avoid non-standard extend;
2020-07-17, by wenzelm
tuned -- avoid non-standard extend/merge;
2020-07-17, by wenzelm
prefer conservative extend/merge of theory naming;
2020-07-17, by wenzelm
support native PID for ML process;
2020-07-16, by wenzelm
merged
2020-07-16, by wenzelm
clarified theory data: more robust merge;
2020-07-16, by wenzelm
proper import sessions;
2020-07-16, by wenzelm
more thorough extend/merge (for Theory.join_theory);
2020-07-16, by wenzelm
more thorough extend/merge (for Theory.join_theory);
2020-07-16, by wenzelm
more thorough extend/merge (for Theory.join_theory);
2020-07-16, by wenzelm
more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
2020-07-16, by wenzelm
more robust: avoid potential problems with encoding of directory name;
2020-07-16, by wenzelm
tuned grouping
2020-07-16, by haftmann
yet another alias
2020-07-16, by haftmann
more robust wrt. experimental changes in Poly/ML;
2020-07-15, by wenzelm
more robust: handle unavailable statistics;
2020-07-15, by wenzelm
merged
2020-07-15, by wenzelm
clarified user counters: expose tasks to external monitor;
2020-07-15, by wenzelm
proper platform path for Windows;
2020-07-15, by wenzelm
clarified signature;
2020-07-15, by wenzelm
support for monitoring of external ML process;
2020-07-15, by wenzelm
clarified signature;
2020-07-15, by wenzelm
more robust;
2020-07-13, by wenzelm
support for monitoring of external ML process;
2020-07-13, by wenzelm
clarified modules: ML_Statistics within bootstrap environment;
2020-07-13, by wenzelm
misc tuning and modernization;
2020-07-13, by wenzelm
clarified examples;
2020-07-13, by wenzelm
concatentation of bit values
2020-07-13, by haftmann
prefer canonically oriented lists of bits and more direct characterizations in definitions
2020-07-12, by haftmann
more simp rules for concrete numerical values
2020-07-12, by haftmann
words added to code generator test
2020-07-12, by haftmann
a generic horner sum operation
2020-07-11, by haftmann
more thms
2020-07-11, by haftmann
clarified message --- as in former ML version (see 940195fbb282);
2020-07-11, by wenzelm
clarified signature;
2020-07-11, by wenzelm
clarified messages: avoid duplicate Timing;
2020-07-11, by wenzelm
clarified messages;
2020-07-11, by wenzelm
clarified signature;
2020-07-11, by wenzelm
tuned;
2020-07-11, by wenzelm
avoid duplicate Timing messages (see also 5c4800f6b25a);
2020-07-11, by wenzelm
more accurate message;
2020-07-11, by wenzelm
tuned;
2020-07-11, by wenzelm
clarified signature;
2020-07-11, by wenzelm
clarified inlined protocol messages;
2020-07-11, by wenzelm
removed unused property;
2020-07-11, by wenzelm
signed_take_bit
2020-07-11, by haftmann
more on single-bit operations
2020-07-11, by haftmann
proper session Timing for build_history log file (see 5c4800f6b25a);
2020-07-10, by wenzelm
clarified signature;
2020-07-10, by wenzelm
more robust, notably for isabelle_cronjob;
2020-07-10, by wenzelm
more robust build_session protocol: allow prover process to terminate/crash without build_session_finished message;
2020-07-10, by wenzelm
Update Metis to 2.4
2020-07-09, by desharna
updated to polyml-5.8.1-20200708: recent repository version for testing;
2020-07-08, by wenzelm
more robust protocol for "Timing ..." messages, notably for pide_session=true;
2020-07-08, by wenzelm
removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible with post-2016 reforms to local theories
2020-07-06, by blanchet
separation of traditional bit operations
2020-07-06, by haftmann
no pide_session on macos: avoid odd "hang" of remote_build_history;
2020-07-05, by wenzelm
support generated preferences, i.e. non-strict system options;
2020-07-05, by wenzelm
factored out auxiliary theory
2020-07-04, by haftmann
prefer explicit proof
2020-07-04, by haftmann
tuned whitespace;
2020-07-03, by wenzelm
use less memory on old hardware;
2020-07-03, by wenzelm
clarified signature;
2020-07-03, by wenzelm
clarified log message (more uniform);
2020-07-03, by wenzelm
misc lemma tuning
2020-07-03, by haftmann
explicit proofs for bit projections
2020-07-03, by haftmann
extraction of equations x = t from premises beneath meta-all
2020-07-02, by haftmann
a small aggiornamento for Z2
2020-07-02, by haftmann
removed superfluous dependency
2020-07-02, by haftmann
factored out ancient numeral representation
2020-07-01, by haftmann
moved to Word_Lib
2020-07-01, by haftmann
more explicit proofs
2020-07-01, by haftmann
clarified options --- potentially more robust;
2020-07-01, by wenzelm
tuned message;
2020-07-01, by wenzelm
clarified signature;
2020-06-27, by wenzelm
more CONTRIBUTORS;
2020-06-26, by wenzelm
more uniform URL (see 60b5a4731695);
2020-06-25, by wenzelm
clarified use of memory: prefer share tree structures over fresh strings;
2020-06-24, by wenzelm
more Java heap space (see 2d658beb815b);
2020-06-24, by wenzelm
clarified NEWS;
2020-06-21, by wenzelm
enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
2020-06-20, by wenzelm
discontinued old AFP test: ancient hardware with insufficient resources;
2020-06-20, by wenzelm
tuned output;
2020-06-20, by wenzelm
merged
2020-06-20, by wenzelm
share cache for parallel sessions;
2020-06-20, by wenzelm
clarified signature;
2020-06-20, by wenzelm
more caching, notably for build/pide_session;
2020-06-20, by wenzelm
removed pointless pide_exports: unused during "build_session" process (reverting 6a64205b491a);
2020-06-20, by wenzelm
tuned --- avoid error in IntelliJ IDEA;
2020-06-19, by wenzelm
simp rules for conversions
2020-06-20, by haftmann
more class operations for the sake of efficient generated code
2020-06-20, by haftmann
merged
2020-06-19, by wenzelm
back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);
2020-06-19, by wenzelm
back to pide_session=false for now, requires too many JVM resources (reverting 026de3424c39);
2020-06-19, by wenzelm
clarified signature;
2020-06-19, by wenzelm
avoid redundant export handling for build;
2020-06-19, by wenzelm
prefer single name
2020-06-19, by haftmann
more lemmas
2020-06-18, by haftmann
build bit operations on word on library theory on bit operations
2020-06-18, by haftmann
bit operations as distinctive library theory
2020-06-18, by haftmann
tweak for code generation
2020-06-18, by haftmann
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
2020-06-18, by haftmann
more lemmas and less name space pollution
2020-06-18, by haftmann
canonical bit shifts for word type, leaving duplicates as they are at the moment
2020-06-18, by haftmann
essential instance about bit structure
2020-06-18, by haftmann
more transfer rules
2020-06-18, by haftmann
dropped yet another duplicate
2020-06-18, by haftmann
fundamental construction of word type following existing transfer rules
2020-06-18, by haftmann
replaced mere alias by input abbreviation
2020-06-18, by haftmann
replaced mere alias by abbreviation
2020-06-18, by haftmann
replaced operation with weak abstraction by input abbreviation
2020-06-18, by haftmann
avoid compound operation
2020-06-18, by haftmann
formal relationships between operations
2020-06-18, by haftmann
eliminated warnings
2020-06-18, by haftmann
replaced mere alias by input abbreviation
2020-06-18, by haftmann
enable pide_session by default;
2020-06-17, by wenzelm
avoid resource problems of JVM by too many parallel XZ compression tasks;
2020-06-17, by wenzelm
interpretations for boolean operators
2020-06-16, by haftmann
more specific thm reference
2020-06-16, by haftmann
clarified errors;
2020-06-13, by wenzelm
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
2020-06-11, by paulson
tuned whitespace;
2020-06-11, by wenzelm
proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;
2020-06-11, by wenzelm
updated to jedit-5.6pre1 (repository version 25349);
2020-06-10, by wenzelm
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
2020-06-10, by blanchet
New Ackermann development
2020-06-09, by paulson
tuned document;
2020-06-08, by wenzelm
proper latex macros, notably for src/HOL/Examples/Iff_Oracle.thy;
2020-06-08, by wenzelm
NEWS;
2020-06-08, by wenzelm
clarified sessions;
2020-06-08, by wenzelm
clarified sessions: "Notable Examples in Isabelle/HOL";
2020-06-08, by wenzelm
clarified sessions: "Notable Examples in Isabelle/Pure";
2020-06-08, by wenzelm
NEWS
2020-06-06, by haftmann
more theorems
2020-06-04, by haftmann
avoid overaggressive default simp rules
2020-06-04, by haftmann
activate simproc for FOL
2020-06-04, by haftmann
more rules for FOL also
2020-06-04, by haftmann
more simp rules
2020-06-04, by haftmann
should have been copied across from Set.thy as well for better printing
2020-06-03, by nipkow
specific atomization inert to later rule set modifications
2020-05-30, by haftmann
more precise scope of atomize
2020-05-30, by haftmann
install simproc but deactivate by default
2020-05-30, by haftmann
adapted to d25093536482;
2020-05-27, by wenzelm
clarified markup;
2020-05-27, by wenzelm
clarified signature;
2020-05-27, by wenzelm
tuned signature;
2020-05-27, by wenzelm
tuned;
2020-05-27, by wenzelm
more NEWS;
2020-05-27, by wenzelm
more documentation on Isabelle/Scala;
2020-05-27, by wenzelm
proper error positions;
2020-05-27, by wenzelm
tuned;
2020-05-27, by wenzelm
tuned whitespace;
2020-05-27, by wenzelm
more antiquotations;
2020-05-27, by wenzelm
check bash functions against Isabelle settings environment;
2020-05-27, by wenzelm
misc tuning;
2020-05-27, by wenzelm
breakable scala_name;
2020-05-27, by wenzelm
tuned signature;
2020-05-26, by wenzelm
discontinued pointless document antiquotation;
2020-05-26, by wenzelm
proper check of example;
2020-05-26, by wenzelm
clarified signature --- fit within limit of 22 arguments;
2020-05-26, by wenzelm
tuned;
2020-05-26, by wenzelm
tuned;
2020-05-26, by wenzelm
more antiquotations;
2020-05-25, by wenzelm
obsolete;
2020-05-25, by wenzelm
check free-form Scala source;
2020-05-25, by wenzelm
clarified static_check: avoid accidental evaluation;
2020-05-25, by wenzelm
omit pointless memoing: Scala compiler is rather bulky anyway;
2020-05-25, by wenzelm
clarified signature;
2020-05-25, by wenzelm
antiquotations for Scala entities;
2020-05-25, by wenzelm
better closeup and more consistent terminology
2020-05-24, by haftmann
merged
2020-05-24, by wenzelm
proper stack_limit;
2020-05-24, by wenzelm
clarified signature;
2020-05-24, by wenzelm
more accurate classpath for "isabelle scala";
2020-05-24, by wenzelm
proper check of registered Scala functions;
2020-05-24, by wenzelm
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
2020-05-24, by wenzelm
clarified build_session protocol;
2020-05-24, by wenzelm
clarified signature;
2020-05-24, by wenzelm
clarified name;
2020-05-24, by wenzelm
more robust: explicit check for PIDE session;
2020-05-24, by wenzelm
tuned signature;
2020-05-24, by wenzelm
unused;
2020-05-24, by wenzelm
tuned signature;
2020-05-23, by wenzelm
check Scala source snippets from ML;
2020-05-23, by wenzelm
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
2020-05-23, by wenzelm
init default context;
2020-05-23, by wenzelm
tuned message;
2020-05-23, by wenzelm
clarified signature;
2020-05-23, by wenzelm
tuned;
2020-05-23, by wenzelm
more brackets (see 2e8af171887f);
2020-05-23, by wenzelm
tuned message;
2020-05-23, by wenzelm
clarified signature;
2020-05-22, by wenzelm
unused;
2020-05-22, by wenzelm
more robust, notably for "isabelle scala";
2020-05-22, by wenzelm
clarified signature;
2020-05-22, by wenzelm
reorganised sorted_set_of_list
2020-05-24, by nipkow
merged
2020-05-24, by nipkow
simpler inductions
2020-05-24, by nipkow
a few new lemmas about functions
2020-05-23, by paulson
comment makes no sense
2020-05-22, by nipkow
added simp lemma
2020-05-22, by nipkow
slightly more specific implementations
2020-05-21, by haftmann
tuned module name space for generated code
2020-05-21, by haftmann
unused alias
2020-05-21, by nipkow
generalized and augmented
2020-05-20, by haftmann
clarified signature;
2020-05-20, by wenzelm
clarified modules;
2020-05-20, by wenzelm
A few new theorems, plus some tidying up
2020-05-20, by paulson
corrected spelling and tuned whitespace
2020-05-20, by haftmann
tuned
2020-05-19, by nipkow
follow Phabricator update 2020 Week 19;
2020-05-18, by wenzelm
another AVL tree version
2020-05-17, by nipkow
added missing preprocessing step for extraction (due to Stefan Berghofer)
2020-05-15, by Manuel Eberl
new HOL simproc: eliminate_false_implies
2020-05-13, by Manuel Eberl
added lemma
2020-05-14, by nipkow
Tuned some proofs in HOL-Analysis
2020-05-14, by Manuel Eberl
The Uniq quantifier for FOL too
2020-05-14, by paulson
generalised pigeonhole principle in HOL-Library.FuncSet
2020-05-13, by Manuel Eberl
new constant power_int in HOL
2020-05-13, by Manuel Eberl
New HOL simproc 'datatype_no_proper_subterm'
2020-05-04, by Manuel Eberl
merged
2020-05-12, by paulson
Fixes for Sup{} = (0::nat)
2020-05-12, by paulson
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
2020-05-12, by paulson
clarified session imports: avoid bulky HOL-Library image;
2020-05-12, by wenzelm
tuned -- avoid warning;
2020-05-12, by wenzelm
"app" -> "join" for RBTs
2020-05-12, by nipkow
"app" -> "join" for uniformity with Join theory; tuned defs
2020-05-12, by nipkow
added top-level functions and tuned
2020-05-11, by nipkow
the Uniq quantifier
2020-05-11, by paulson
modernized notation for bit operations
2020-05-09, by haftmann
merged
2020-05-08, by nipkow
avoid hidden undef cases
2020-05-08, by nipkow
explicit mask operation for bits
2020-05-08, by haftmann
prefer _ mod 2 over of_bool (odd _)
2020-05-08, by haftmann
less aggressive default simp rules
2020-05-08, by haftmann
simplified and tuned
2020-05-06, by nipkow
tuned
2020-05-06, by nipkow
tuned
2020-05-06, by nipkow
tuned proofs
2020-05-05, by nipkow
tuned var. names
2020-05-05, by nipkow
tuned var. names
2020-05-04, by nipkow
AVL trees with balance tags
2020-05-04, by nipkow
A little more tidying up
2020-04-29, by paulson
tuned
2020-04-29, by nipkow
merged
2020-04-28, by nipkow
tuned
2020-04-28, by nipkow
merged
2020-04-28, by wenzelm
added "isabelle sessions" tool;
2020-04-28, by wenzelm
tuned messages;
2020-04-28, by wenzelm
use abs(h l - h r) instead of 3 cases, tuned proofs
2020-04-28, by nipkow
added lemmas
2020-04-27, by nipkow
simplified construction of binary bit operations
2020-04-27, by haftmann
temporarily revert change which does not work as expected
2020-04-25, by haftmann
more rules
2020-04-25, by haftmann
added Height_Balanced_Trees
2020-04-25, by nipkow
documentation of relevant ideas
2020-04-24, by haftmann
numeral rules for take_bit / drop_bit on int
2020-04-24, by haftmann
opaque export does not work as expected in presence of dependent instances
2020-04-24, by haftmann
merged
2020-04-23, by nipkow
tuned document
2020-04-23, by nipkow
split AVL_Set.thy
2020-04-23, by nipkow
avoid passing chained facts twice to preplay in Sledgehammer
2020-04-23, by blanchet
tweaked Vampire's options + tuning
2020-04-23, by blanchet
more robust Isabelle_System.init (amending c0bc99aad936): avoid non-termination on Windows (java.lang.StackOverflowError);
2020-04-23, by wenzelm
back to more modest (but uniform) Java stack, see 97fc4f657bda;
2020-04-23, by wenzelm
more generous Java memory, also hoping to prevent spurious java.lang.StackOverflowError in isabelle_cronjob;
2020-04-23, by wenzelm
added lemmas
2020-04-23, by nipkow
hooks for foundational terms: protection of foundational terms during simplification
2020-04-21, by haftmann
merged
2020-04-22, by wenzelm
merged
2020-04-22, by wenzelm
avoid deprecated operations;
2020-04-22, by wenzelm
tuned -- avoid odd compiler warning;
2020-04-22, by wenzelm
avoid deprecated operations;
2020-04-22, by wenzelm
deprecated and obsolete;
2020-04-22, by wenzelm
tuned signature -- avoid warnings;
2020-04-22, by wenzelm
more informative error;
2020-04-22, by wenzelm
new funs successive and distinct_adj
2020-04-22, by nipkow
added lemmas
2020-04-22, by nipkow
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
2020-04-21, by wenzelm
clarified signature -- avoid warning;
2020-04-21, by wenzelm
tuned;
2020-04-21, by wenzelm
clarified imports;
2020-04-21, by wenzelm
more robust judgment handling
2020-04-20, by haftmann
Sketch and explore again
2020-04-19, by paulson
removal of symmetries in Polytope, plus some tidying
2020-04-19, by paulson
Sketch_and_Explore — oops
2020-04-19, by paulson
the rest of the applys
2020-04-19, by paulson
more applys
2020-04-18, by paulson
merged
2020-04-17, by paulson
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
2020-04-17, by paulson
discontinued somewhat incoherent patches (see also 3b36fc4916af);
2020-04-17, by wenzelm
use friendlier package;
2020-04-17, by wenzelm
removed LaTeX package and hack to avoid ALLCAPS headers
2020-04-17, by blanchet
use friendlier package
2020-04-17, by blanchet
move virtual machine node;
2020-04-16, by wenzelm
generalized
2020-04-16, by haftmann
more theorems
2020-04-16, by haftmann
another rule on numerals
2020-04-16, by haftmann
bit on numerals
2020-04-16, by haftmann
more complete rules on numerals
2020-04-16, by haftmann
more complete rules on numerals
2020-04-16, by haftmann
removed obsolete RC tags;
2020-04-16, by wenzelm
merged
2020-04-15, by wenzelm
Added tag Isabelle2020 for changeset abf3e80bd815
2020-04-15, by wenzelm
tuned NEWS;
Isabelle2020
2020-04-13, by wenzelm
tuned NEWS;
2020-04-12, by wenzelm
tuned message;
2020-04-13, by wenzelm
tuned message;
2020-04-13, by wenzelm
clarified signature;
2020-04-13, by wenzelm
more cleaning up Homotopy
2020-04-12, by paulson
cleaning up Homotopy
2020-04-12, by paulson
merged
2020-04-10, by paulson
more removal of applys
2020-04-10, by paulson
avoid hard-wired stuff: configure via plugin services;
2020-04-09, by wenzelm
tuned;
2020-04-09, by wenzelm
tuned;
2020-04-09, by wenzelm
clarified init of settings vs. services;
2020-04-08, by wenzelm
tuned message;
2020-04-08, by wenzelm
merged
2020-04-08, by wenzelm
another isabelle_scala_service;
2020-04-08, by wenzelm
tuned;
2020-04-08, by wenzelm
tuned -- avoid deprecated operations;
2020-04-08, by wenzelm
more general support for isabelle_scala_service;
2020-04-08, by wenzelm
merged
2020-04-08, by wenzelm
merged
2020-04-08, by wenzelm
Added tag Isabelle2020-RC5 for changeset 8ed68b2aeba1
2020-04-08, by wenzelm
more robust: notably for sledgehammer with 'using' and prover=cvc4;
2020-04-04, by wenzelm
NEWS;
2020-04-07, by wenzelm
more careful handling of interrupts, notably for Isabelle/jEdit Scala Console;
2020-04-07, by wenzelm
clarified signature: more uniform treatment of stopped/interrupted state;
2020-04-07, by wenzelm
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
2020-04-07, by wenzelm
tuned signature --- avoid confusion with init_view(buffer: Buffer, text_area: JEditTextArea);
2020-04-07, by wenzelm
merged
2020-04-07, by nipkow
more automation and clarification
2020-04-07, by nipkow
merged
2020-04-07, by paulson
removed more applys
2020-04-06, by paulson
merged;
2020-04-06, by wenzelm
more robust interrupts;
2020-04-06, by wenzelm
tuned message;
2020-04-06, by wenzelm
tuned;
2020-04-06, by wenzelm
NEWS;
2020-04-06, by wenzelm
tuned;
2020-04-06, by wenzelm
more robust interrupt handling;
2020-04-06, by wenzelm
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
2020-04-06, by wenzelm
clarified signature;
2020-04-06, by wenzelm
clarified signature;
2020-04-06, by wenzelm
more uniform and Java-conformant: change of handler is non-blocking and interrupts should not be exposed prematurely (reverting 220d19f3e074);
2020-04-06, by wenzelm
terminate faster;
2020-04-06, by wenzelm
tuned;
2020-04-06, by wenzelm
tuned;
2020-04-06, by wenzelm
clarified interrupt handling;
2020-04-06, by wenzelm
clarified modules;
2020-04-06, by wenzelm
tuned;
2020-04-06, by wenzelm
misc tuning and clarification;
2020-04-06, by wenzelm
more general interrupt_handler, with some cascading;
2020-04-05, by wenzelm
clarified signature;
2020-04-05, by wenzelm
a few more applys
2020-04-06, by paulson
fixed a broken frac_le proof
2020-04-06, by paulson
fixed more nasty proofs
2020-04-05, by paulson
merged
2020-04-05, by paulson
Tidied up more ancient, horrible proofs. Liberalised frac_le
2020-04-05, by paulson
clarified signature: more uniform ML vs. Scala;
2020-04-05, by wenzelm
clarified names;
2020-04-05, by wenzelm
clarified names;
2020-04-05, by wenzelm
proper use of flag;
2020-04-04, by wenzelm
clarified signature;
2020-04-04, by wenzelm
tuned names;
2020-04-04, by wenzelm
finally expose interrupt, similar to ML;
2020-04-04, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-768
+768
+1000
+3000
tip