isabelle: Graph

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
Standard_Thread for isabelle command-line tools;
2020-04-04, by wenzelm
tuned -- Command_Line.tool is already part of Isabelle_Tool;
2020-04-04, by wenzelm
clarified signature;
2020-04-04, by wenzelm
clarified signature;
2020-04-04, by wenzelm
thread pool with Standard_Thread workers;
2020-04-04, by wenzelm
clarified signature;
2020-04-04, by wenzelm
support for uninterruptible execution;
2020-04-04, by wenzelm
tuned -- prefer Config.T over Data;
2020-04-03, by wenzelm
proper "editor_tracing_messages=0" as in "isabelle dump";
2020-04-03, by wenzelm
tuned;
2020-04-03, by wenzelm
clarified build_options vs. job options;
2020-04-03, by wenzelm
more official handling of protocol messages, including export;
2020-04-03, by wenzelm
less redundant markup reports;
2020-04-03, by wenzelm
more accurate context position reports;
2020-04-03, by wenzelm
clarified signature;
2020-04-03, by wenzelm
clarified signature;
2020-04-03, by wenzelm
tuned;
2020-04-03, by wenzelm
clarified signature;
2020-04-03, by wenzelm
tuned signature;
2020-04-03, by wenzelm
proper treatment of startup errors, notably for Pure ROOT.ML;
2020-04-02, by wenzelm
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
2020-04-02, by wenzelm
merged
2020-04-02, by wenzelm
Added tag Isabelle2020-RC4 for changeset 1f3d9a9dd42a
2020-04-02, by wenzelm
more robust, notably wrt. interrupts;
2020-03-28, by wenzelm
merged
2020-03-26, by wenzelm
more NEWS;
2020-03-25, by wenzelm
clarified messages: indicate termination explicitly;
2020-03-25, by wenzelm
avoid vacous type variable, due to "potentially redundant" shyps in Thm.unconstrainT;
2020-03-24, by wenzelm
Added tag Isabelle2020-RC3 for changeset 7fe1a344404a
2020-03-23, by wenzelm
updated to current cygwin-20200323, after 3.1.4-1 from 19-Feb-2020;
2020-03-23, by wenzelm
avoid jdk-11.0.6+10: it shows problem "S8217731: Font rendering and glyph spacing changed from jdk-8 to jdk-11" https://bugs.openjdk.java.net/browse/JDK-8217731 even though the changelog claims to have resolved this;
2020-03-22, by wenzelm
clarified signature: more direct Isabelle_Process.EXIT;
2020-04-02, by wenzelm
proper arguments of protocol function;
2020-04-02, by wenzelm
merged
2020-04-01, by wenzelm
more robust: process stdout on Windows may contain CR;
2020-04-01, by wenzelm
clarified signature;
2020-04-01, by wenzelm
prefer system option: easier to make it default;
2020-04-01, by wenzelm
support multiple sessions, notably for "isabelle build -P -j2";
2020-04-01, by wenzelm
pretty formatting as in Isabelle/ML;
2020-04-01, by wenzelm
output prover messages;
2020-04-01, by wenzelm
clarified signature;
2020-04-01, by wenzelm
clarified signature: more robust;
2020-04-01, by wenzelm
proper parent base;
2020-04-01, by wenzelm
traditional print_mode for batch build;
2020-04-01, by wenzelm
proper support for "isabelle build -P Pure";
2020-04-01, by wenzelm
clarified signature: more robust bootstrap base;
2020-04-01, by wenzelm
proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
2020-04-01, by wenzelm
proper context for loading Pure;
2020-04-01, by wenzelm
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
2020-03-31, by wenzelm
close socket explicitly (idempotent);
2020-03-31, by wenzelm
more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
2020-03-31, by wenzelm
simplified code and proofs
2020-04-01, by nipkow
automated proof
2020-04-01, by nipkow
merged
2020-03-31, by nipkow
cleaned proofs
2020-03-31, by nipkow
clarified signature;
2020-03-30, by wenzelm
more accurate treatment of errors;
2020-03-30, by wenzelm
clarified modules: global quasi-scope for markers;
2020-03-30, by wenzelm
redunant simp rule
2020-03-30, by nipkow
merged
2020-03-29, by paulson
more ugly old proofs
2020-03-29, by paulson
merged
2020-03-29, by wenzelm
tuned;
2020-03-29, by wenzelm
clarified modules;
2020-03-29, by wenzelm
clarified signature: more explicit type Protocol_Message.Marker;
2020-03-29, by wenzelm
tuned signature -- follow Scala;
2020-03-29, by wenzelm
tuned;
2020-03-29, by wenzelm
more explicit type Protocol_Message.Marker;
2020-03-29, by wenzelm
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
2020-03-29, by wenzelm
tuned;
2020-03-29, by wenzelm
tuned whitespace;
2020-03-29, by wenzelm
more tidying up of old apply-proofs
2020-03-29, by paulson
merged
2020-03-28, by wenzelm
tuned;
2020-03-28, by wenzelm
tuned;
2020-03-28, by wenzelm
tuned;
2020-03-28, by wenzelm
eliminated pointless flag (see also 6533ceee4cd7);
2020-03-28, by wenzelm
tuned;
2020-03-28, by wenzelm
merged
2020-03-28, by paulson
structured a lot of ancient, horrible proofs
2020-03-28, by paulson
clarified Isabelle_Process phases;
2020-03-28, by wenzelm
clarified order: update syslog before handling exit;
2020-03-28, by wenzelm
tuned error message;
2020-03-28, by wenzelm
clarified signature: more robust startup_join;
2020-03-28, by wenzelm
merged
2020-03-27, by wenzelm
tuned;
2020-03-27, by wenzelm
misc tuning based on hints by IntelliJ IDEA;
2020-03-27, by wenzelm
clarified signature;
2020-03-27, by wenzelm
clarified signature;
2020-03-27, by wenzelm
clarified signature;
2020-03-27, by wenzelm
clarified signature;
2020-03-27, by wenzelm
tuned;
2020-03-27, by wenzelm
clarified signature: more accurate session_base_info.sessions_structure;
2020-03-27, by wenzelm
clarified signature;
2020-03-27, by wenzelm
added lemma
2020-03-27, by nipkow
merged
2020-03-25, by paulson
updated to more modern style
2020-03-25, by paulson
updated to scala-2.12.11;
2020-03-23, by wenzelm
merged
2020-03-23, by paulson
put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2
2020-03-23, by paulson
merged
2020-03-22, by paulson
new-style Greater lemmas
2020-03-22, by paulson
tidying up some horrible proofs
2020-03-22, by paulson
avoid jdk-11.0.6+10: it shows problem "S8217731: Font rendering and glyph spacing changed from jdk-8 to jdk-11" https://bugs.openjdk.java.net/browse/JDK-8217731 even though the changelog claims to have resolved this;
2020-03-22, by wenzelm
tuned;
2020-03-22, by wenzelm
merged;
2020-03-21, by wenzelm
more NEWS;
2020-03-21, by wenzelm
delete Isabelle distribution archive after use;
2020-03-21, by wenzelm
documentation for "isabelle build_docker";
2020-03-21, by wenzelm
updated for release;
2020-03-21, by wenzelm
tuned bib;
2020-03-21, by wenzelm
more documentation on view.antiAlias, not just NEWS;
2020-03-21, by wenzelm
more NEWS;
2020-03-20, by wenzelm
avoid premature crash due to missing session parents/imports;
2020-03-20, by wenzelm
avoid accidental update of base session sources (following documentation in "system" manual);
2020-03-20, by wenzelm
avoid duplicate stderr output in isabelle build -v, e.g. "Timing ..." (amending a829207b32a3);
2020-03-20, by wenzelm
prefer subpixel antialiasing by default: rendering of text is usually much faster, notably on Linux (see also 093ab1a99eb6 and f610115ca3d0);
2020-03-20, by wenzelm
slightly more explicit error, without going into the graph of proof futures;
2020-03-18, by wenzelm
more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);
2020-03-18, by wenzelm
prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as proposed by Pedro Sánchez Terraf;
2020-03-18, by wenzelm
tuned documentation, based on hints by Pedro Sánchez Terraf;
2020-03-18, by wenzelm
backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;
2020-03-18, by wenzelm
back to old-style names for uniform sorting of build_status (amending 138e8226961e);
2020-03-19, by wenzelm
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
2020-03-19, by wenzelm
clarified connection parameters (again, after adjusting $HOME/.ssh configuration);
2020-03-18, by wenzelm
clarified output;
2020-03-18, by wenzelm
proper host for ssh.hg_url (required aliasing works via $HOME/.ssh/config);
2020-03-16, by wenzelm
clarified connection parameters;
2020-03-16, by wenzelm
clarified test;
2020-03-15, by wenzelm
remove Thm.transfer workaround made obsplete by cf2406e654cf
2020-03-15, by traytel
back to post-release mode;
2020-03-15, by wenzelm
Added tag Isabelle2020-RC2 for changeset 7eadccd4392c
2020-03-15, by wenzelm
claried error elements: include internalized errors of tokens/commands;
2020-03-15, by wenzelm
more robust connection via proxy_host;
2020-03-15, by wenzelm
more robust: proper transfer if Context.eq_thy_id;
2020-03-14, by wenzelm
merged
2020-03-14, by wenzelm
tuned;
2020-03-14, by wenzelm
tuned;
2020-03-14, by wenzelm
more robust hg_url;
2020-03-14, by wenzelm
proper usage (amending 8c7706b053c7);
2020-03-13, by wenzelm
proper escape for literal single quotes;
2020-03-13, by wenzelm
some uses of "' " as witness for this feature;
2020-03-13, by wenzelm
allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
2020-03-13, by wenzelm
tidied up a few little proofs
2020-03-14, by paulson
updated for release;
2020-03-12, by wenzelm
more usable defaults for high resolution on Linux, where the desktop environment usually lacks automatic scaling;
2020-03-12, by wenzelm
tuned for Isabelle2020;
2020-03-12, by wenzelm
more explicit defaults;
2020-03-12, by wenzelm
proper transfer for Thm.derivation_name;
2020-03-12, by wenzelm
tuned OS names;
2020-03-10, by wenzelm
standard tests for macOS 10.15 Catalina;
2020-03-10, by wenzelm
updated NEWS w.r.t. e0237f2eb49d
2020-03-10, by Manuel Eberl
more frugal simp rules for bit operations; more pervasive use of bit selector
2020-03-08, by haftmann
more scalable output of YXML files;
2020-03-09, by wenzelm
proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;
2020-03-09, by wenzelm
tuned;
2020-03-09, by wenzelm
tuned whitespace;
2020-03-09, by wenzelm
more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);
2020-03-09, by wenzelm
clarified;
2020-03-09, by wenzelm
tuned signature;
2020-03-09, by wenzelm
tuned signature;
2020-03-09, by wenzelm
tuned signature;
2020-03-09, by wenzelm
tuned;
2020-03-07, by wenzelm
copy jEdit sources instead of jar, for better browsing experience;
2020-03-07, by wenzelm
proper option;
2020-03-07, by wenzelm
tuned;
2020-03-06, by wenzelm
formally depend on Java 11 --- discontinue Java 8 workaround;
2020-03-06, by wenzelm
support Java/VM monitoring via jconsole;
2020-03-06, by wenzelm
escape some special chars, notably for URL#NAME form;
2020-03-04, by wenzelm
library theory for extractions of equations x = t into premises
2020-03-03, by haftmann
tuned
2020-03-03, by haftmann
rebuild x86_64-linux on Ubuntu 14.04.6 LTS;
2020-03-04, by wenzelm
merged
2020-03-03, by wenzelm
include actions for jEdit dockables, e.g. "vfs.browser";
2020-03-03, by wenzelm
misc tuning and clarification;
2020-03-03, by wenzelm
infrastructure for extraction of equations x = t from premises beneath meta-all
2020-03-02, by haftmann
avoid conflict with isabelle.next-error, resulting in odd startup dialog;
2020-03-03, by wenzelm
updated for release;
2020-03-03, by wenzelm
Added tag Isabelle2020-RC1 for changeset a8849ac415cc
2020-03-02, by wenzelm
follow Phabricator update 2020 Week 6;
2020-03-02, by wenzelm
tuned signature;
2020-03-02, by wenzelm
VSCode extension for official Isabelle release;
2020-03-02, by wenzelm
more documentation;
2020-03-02, by wenzelm
tuned GUI;
2020-03-02, by wenzelm
clarified command line;
2020-03-01, by wenzelm
proper navigation wrt. caret;
2020-03-01, by wenzelm
clarified modifier: avoid confusion of CS+a as C+a;
2020-03-01, by wenzelm
tuned -- avoid deprecated operations;
2020-03-01, by wenzelm
more Isabelle/jEdit actions;
2020-03-01, by wenzelm
updated for release;
2020-03-01, by wenzelm
more Isabelle/jEdit actions;
2020-02-29, by wenzelm
tuned signature;
2020-02-29, by wenzelm
tuned;
2020-02-29, by wenzelm
tuned lift_bnf's user interface for quotients
2020-02-28, by traytel
NEWS;
2020-02-28, by wenzelm
updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
2020-02-28, by wenzelm
tuned;
2020-02-28, by wenzelm
more complete signature;
2020-02-27, by wenzelm
more complete signature;
2020-02-27, by wenzelm
clarified versions -- more reproducible build;
2020-02-27, by wenzelm
removed dead lemma
2020-02-27, by nipkow
simplified proofs
2020-02-26, by nipkow
updated for release;
2020-02-26, by wenzelm
updated for release;
2020-02-26, by wenzelm
merged
2020-02-26, by wenzelm
updated for release;
2020-02-26, by wenzelm
updated version;
2020-02-26, by wenzelm
obsolete;
2020-02-26, by wenzelm
less ambitious preview: discontinued preview-update / preview-source which did not work on the spot via WebviewPanel;
2020-02-26, by wenzelm
misc tuning and clarification;
2020-02-26, by wenzelm
obsolete;
2020-02-26, by wenzelm
proper message passing -- discontinued obsolete auxiliary commands;
2020-02-26, by wenzelm
clarified Panel;
2020-02-25, by wenzelm
removed duplicate (amending 5763d9a2f47d, 5aa9cb83e70e);
2020-02-25, by wenzelm
update to WebviewPanel API, following initial version by Peter Zeller;
2020-02-25, by wenzelm
Moved a number of general-purpose lemmas into HOL
2020-02-26, by paulson
more robust shutdown while Isabelle_Process is starting up, e.g. quit after dialog Isabelle version for testing";
2020-02-25, by wenzelm
merged
2020-02-24, by traytel
lift BNF witnesses for quotients (unless better ones are specified by the user)
2020-02-24, by traytel
more robust (amending add9a9f6a290): proper syntax error instead of exception for grammar with unreachable nonterminals, e.g. nonterminal f1 syntax "_F" :: "f1 ⇒ 'b" ("F _" 10);
2020-02-24, by wenzelm
merged
2020-02-24, by nipkow
tuned var names (avoid h)
2020-02-24, by nipkow
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
2020-02-24, by wenzelm
a few new lemmas
2020-02-24, by paulson
tuned deletion
2020-02-21, by nipkow
merged
2020-02-20, by traytel
additional lemmas about alw and suntil (by Michael Foster)
2020-02-19, by traytel
proper print mode for function_space notation (amending d68b705719ce);
2020-02-19, by wenzelm
proper file name (amending ce3409dfb18c);
2020-02-19, by wenzelm
merged
2020-02-18, by nipkow
tuned proof
2020-02-18, by nipkow
more robust pretty printing of broken YXML, e.g. single "\^E";
2020-02-18, by wenzelm
merged
2020-02-17, by wenzelm
proper sort constraints for strip_shyps, for sort relations used in minimization;
2020-02-17, by wenzelm
merged
2020-02-17, by paulson
a few new lemmas
2020-02-17, by paulson
tuned;
2020-02-17, by wenzelm
merged
2020-02-16, by nipkow
lemmas about "card A = 2"; prefer iff to implications
2020-02-16, by nipkow
NEWS;
2020-02-16, by wenzelm
proper sort constraints for strip_shyps, which implicitly performs type instantiation;
2020-02-16, by wenzelm
NEWS;
2020-02-15, by wenzelm
Added tag Isabelle2020-RC0 for changeset 21c0b3a9d2f8
2020-02-14, by wenzelm
added lemmas
2020-02-13, by nipkow
canonical approach towards lifting
2020-02-13, by haftmann
more instances
2020-02-11, by haftmann
tuned proof
2020-02-11, by haftmann
afford newer Mercurial version, just before odd problems in 4.0 and 4.1;
2020-02-12, by wenzelm
afford more logging (following defaults on Ubuntu);
2020-02-12, by wenzelm
updated for release;
2020-02-11, by wenzelm
tuned;
2020-02-11, by wenzelm
updated for release;
2020-02-11, by wenzelm
some lemmas about the lex ordering on lists, etc.
2020-02-11, by paulson
proper symbols;
2020-02-10, by wenzelm
NEWS;
2020-02-10, by wenzelm
recover from Unicode accident in 4abd07cd034f;
2020-02-10, by wenzelm
updated for release;
2020-02-10, by wenzelm
NEWS;
2020-02-10, by wenzelm
NEWS;
2020-02-10, by wenzelm
tuned;
2020-02-10, by wenzelm
tuned;
2020-02-10, by wenzelm
easy abstraction over pointwise bit operations
2020-02-09, by haftmann
more rules for natural deduction from inequalities
2020-02-09, by haftmann
rule concerning bit (push_bit ...)
2020-02-09, by haftmann
more lemmas
2020-02-09, by haftmann
allow to override repository versions at runtime;
2020-02-08, by wenzelm
follow Phabricator update 2020 Week 5;
2020-02-07, by wenzelm
simplified logical constructions
2020-02-05, by haftmann
simplified logical constructions
2020-02-05, by haftmann
more theorems
2020-02-03, by haftmann
Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf
2020-02-04, by paulson
tuned
2020-02-04, by nipkow
tuned
2020-02-03, by nipkow
added Interval_Tree.thy
2020-02-03, by nipkow
more specific class assumptions
2020-02-01, by haftmann
more theorems
2020-02-01, by haftmann
ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9);
2020-01-28, by wenzelm
Tidied up some messy proofs
2020-01-28, by paulson
sketches of ideas still to come
2020-01-26, by haftmann
more theorems
2020-01-26, by haftmann
generalized
2020-01-26, by haftmann
tuned
2020-01-26, by haftmann
Two lemmas about nsets
2020-01-27, by paulson
A few lemmas connected with orderings
2020-01-27, by paulson
tuned
2020-01-22, by haftmann
tuned
2020-01-22, by haftmann
dropped dead code
2020-01-22, by haftmann
merged
2020-01-22, by nipkow
added lemma
2020-01-22, by nipkow
Removed multiplicativity assumption from normalization_semidom
2020-01-21, by Manuel Eberl
clarified file names;
2020-01-19, by wenzelm
clarified build_polyml_component: include IDE entry point for ML compiler;
2020-01-19, by wenzelm
merged
2020-01-19, by wenzelm