isabelle: Graph

proper build for fresh target directory (amending d9823224fcfe); default tip
47 minutes ago, by wenzelm
put more resources into jedit_build component;
61 minutes ago, by wenzelm
more brackets (see f6b453449cc6);
3 hours ago, by wenzelm
more brackets;
4 hours ago, by wenzelm
proper settings variable, amending 6e85281177df;
6 hours ago, by wenzelm
merged
6 hours ago, by wenzelm
tuned proofs --- avoid z3, which is absent on arm64-linux;
7 hours ago, by wenzelm
proper condition: z3 could be absent, e.g. on arm64-linux;
8 hours ago, by wenzelm
build auxiliary jEdit component in Isabelle/Scala;
10 hours ago, by wenzelm
separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);
2 days ago, by wenzelm
tuned message;
2 days ago, by wenzelm
clarified signature;
2 days ago, by wenzelm
tuned signature;
3 days ago, by wenzelm
more elementary swap
39 hours ago, by haftmann
tuned comments;
3 days ago, by wenzelm
misc updates and clarification;
3 days ago, by wenzelm
clarified file name;
3 days ago, by wenzelm
merged
3 days ago, by wenzelm
updated to polyml-5.8.2 (official release);
3 days ago, by wenzelm
clarified default_platform_families (again);
3 days ago, by wenzelm
proper option for linux_arm;
3 days ago, by wenzelm
proper "$?";
3 days ago, by wenzelm
proper jvm_platform, notably for org.sqlite.lib.path;
3 days ago, by wenzelm
tuned message;
3 days ago, by wenzelm
support for platform family "linux_arm";
4 days ago, by wenzelm
clarified purge;
4 days ago, by wenzelm
removed junk;
4 days ago, by wenzelm
support local build_heaps;
4 days ago, by wenzelm
merged
5 days ago, by wenzelm
tuned --- rename = dist_name is sufficient;
5 days ago, by wenzelm
proper dist_name;
5 days ago, by wenzelm
clarified option -P: allow empty argument;
5 days ago, by wenzelm
support for existing release archive;
5 days ago, by wenzelm
tuned signature;
5 days ago, by wenzelm
clarified signature;
5 days ago, by wenzelm
more website content;
6 days ago, by wenzelm
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
6 days ago, by wenzelm
tuned signature;
6 days ago, by wenzelm
tuned theory structure
5 days ago, by haftmann
more appropriate location
5 days ago, by haftmann
collected lemmas on permutations
6 days ago, by haftmann
A nice cardinality lemma
7 days ago, by paulson
tuned
7 days ago, by nipkow
more robust indentation: proper line context after insert;
8 days ago, by wenzelm
more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
8 days ago, by wenzelm
support nested cases;
8 days ago, by wenzelm
tuned;
8 days ago, by wenzelm
tuned;
8 days ago, by wenzelm
early definition of ML antiquotations;
8 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
clarified signature: more operations;
11 days ago, by wenzelm
clarified signature: more operations;
11 days ago, by wenzelm
clarified signature;
11 days ago, by wenzelm
tuned signature;
12 days ago, by wenzelm
clarified command-line, following other build_XYZ tools;
12 days ago, by wenzelm
more recent OCaml and GHC stack: better support for Apple Silicon;
12 days ago, by wenzelm
merged
2 weeks ago, by wenzelm
avoid "exec" to change the winpid;
2 weeks ago, by wenzelm
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
2 weeks ago, by wenzelm
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
rebuild executable for x86_64-darwin;
2 weeks ago, by wenzelm
clarified command-line;
2 weeks ago, by wenzelm
update Linux base-line;
2 weeks ago, by wenzelm
tuned comments;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
simplified typesetting of \<guillemotleft>...\<guillemotright>;
2 weeks ago, by wenzelm
collecting more lemmas concerning multisets
2 weeks ago, by haftmann
proper use of antiquotations;
2 weeks ago, by wenzelm
more documentation on "Conversions";
3 weeks ago, by wenzelm
tuned
3 weeks ago, by nipkow
updated example;
3 weeks ago, by wenzelm
clarified options (again);
3 weeks ago, by wenzelm
more options: update ISABELLE_IDENTIFIER;
3 weeks ago, by wenzelm
clarified conditional ML;
3 weeks ago, by wenzelm
support for conditional ML text;
3 weeks ago, by wenzelm
updated example;
3 weeks ago, by wenzelm
clarified options;
3 weeks ago, by wenzelm
proper context variable handling when stripping leadings quantifiers from test goals
3 weeks ago, by haftmann
proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);
3 weeks ago, by wenzelm
eliminated perl: prefer elementary GNU printenv;
3 weeks ago, by wenzelm
more robust bootstrap of components;
3 weeks ago, by wenzelm
more self-contained support for macOS;
3 weeks ago, by wenzelm
misc tuning and clarification;
3 weeks ago, by wenzelm
tuned signature;
3 weeks ago, by wenzelm
support for base64 via Isabelle/Scala/ML;
4 weeks ago, by wenzelm
compile;
4 weeks ago, by wenzelm
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
4 weeks ago, by wenzelm
clarified signature (again);
4 weeks ago, by wenzelm
merged
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
unused;
4 weeks ago, by wenzelm
unused;
4 weeks ago, by wenzelm
clarified signature: more structured arguments, notably for remote provers;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
clarified signature: avoid tmp file;
4 weeks ago, by wenzelm
clarified signature for Scala functions;
4 weeks ago, by wenzelm
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
clarified cache;
4 weeks ago, by wenzelm
clarified signature: Bytes extends CharSequence already (see d201996f72a8);
4 weeks ago, by wenzelm
clarified exceptions;
4 weeks ago, by wenzelm
more uniform use of Byte_Message;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
more robust treatment of empty markup: it allows to produce formal chunks;
4 weeks ago, by wenzelm
collected combinatorial material
4 weeks ago, by haftmann
tuned;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
more documentation;
4 weeks ago, by wenzelm
proper treatment of nested antiquotations;
4 weeks ago, by wenzelm
support for ML special forms: modified evaluation similar to Scheme;
4 weeks ago, by wenzelm
clarified signature: more detailed token positions for antiquotations;
4 weeks ago, by wenzelm
merged
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
confluent preprocessing for floats in presence of target language numerals
4 weeks ago, by haftmann
subclass relation
4 weeks ago, by haftmann
some tinkering with npm versions;
4 weeks ago, by wenzelm
some tinkering with npm versions;
4 weeks ago, by wenzelm
back to post-release mode;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
auto-update due to "isabelle build_vscode";
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned --- following hints by IntelliJ IDEA;
4 weeks ago, by wenzelm
fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes)
4 weeks ago, by Manuel Eberl
simplified definition
4 weeks ago, by haftmann
new lemmas
4 weeks ago, by haftmann
discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove";
5 weeks ago, by wenzelm
following recent Phabricator update, after 2021 Week 13 (Late March);
5 weeks ago, by wenzelm
merged
5 weeks ago, by paulson
Cosmetic: no !! in the lemma statement
5 weeks ago, by paulson
clarified README;
5 weeks ago, by wenzelm
more standard header, with utf-8 encoding;
5 weeks ago, by wenzelm
clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
5 weeks ago, by wenzelm
merged
5 weeks ago, by nipkow
new automatic order prover: stateless, complete, verified
5 weeks ago, by nipkow
clarified signature;
5 weeks ago, by wenzelm
clarified: follow "isabelle version -t";
5 weeks ago, by wenzelm
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
5 weeks ago, by wenzelm
tuned signature -- more explicit types;
5 weeks ago, by wenzelm
more robust and uniform ISABELLE_TAGS;
5 weeks ago, by wenzelm
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
5 weeks ago, by wenzelm
simplified release status (again), in contrast to a43898f76ae9;
5 weeks ago, by wenzelm
more uniform HTTP resources;
5 weeks ago, by wenzelm
clarified (again): local tip could be actually more recent;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
clarified name;
5 weeks ago, by wenzelm
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
5 weeks ago, by wenzelm
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
5 weeks ago, by wenzelm
updated to latest latex due to new mechanism for dealing with bold ccfonts
5 weeks ago, by nipkow
removal of needless hypothesis in hd_rev and last_rev
6 weeks ago, by paulson
more robust;
6 weeks ago, by wenzelm
clarified message;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
tuned message;
6 weeks ago, by wenzelm
proper export;
6 weeks ago, by wenzelm
more options: build is part of default setup;
6 weeks ago, by wenzelm
misc tuning and clarification;
6 weeks ago, by wenzelm
more options;
6 weeks ago, by wenzelm
proper Admin script, outside the settings environment;
6 weeks ago, by wenzelm
tuned whitespace;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
clarified;
6 weeks ago, by wenzelm
tuned message;
6 weeks ago, by wenzelm
tuned message;
6 weeks ago, by wenzelm
more accurate settings after update of current version;
6 weeks ago, by wenzelm
clarified messages;
6 weeks ago, by wenzelm
more robust: lest hg work out remote tip;
6 weeks ago, by wenzelm
more options;
6 weeks ago, by wenzelm
clarified treatment of multiple versions: last one counts;
6 weeks ago, by wenzelm
more robust;
6 weeks ago, by wenzelm
more robust: explicit repository root;
6 weeks ago, by wenzelm
more robust;
6 weeks ago, by wenzelm
more convenient repository setup;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
more robust invocation of hg;
6 weeks ago, by wenzelm
more robust: idempotent;
6 weeks ago, by wenzelm
more robust invocation of hg;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
clarified output;
6 weeks ago, by wenzelm
support repository archives (without full .hg directory);
6 weeks ago, by wenzelm
more robust invocation of hg;
6 weeks ago, by wenzelm
record official releases that follow a certain structure, with public access via https://isabelle.sketis.net/repos/isabelle/raw-file/tip/Admin/Release/official (NB: Isabelle2013-1 had to be retracted);
6 weeks ago, by wenzelm
dedicated session for combinatorial material
6 weeks ago, by haftmann
support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;
6 weeks ago, by wenzelm
enforce full build;
6 weeks ago, by wenzelm
turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;
6 weeks ago, by wenzelm
discontinue fragile check in LaTeX, e.g. problems with toc entries;
6 weeks ago, by wenzelm
merged
6 weeks ago, by paulson
merged
7 weeks ago, by paulson
type class relaxation
7 weeks ago, by paulson
more NEWS;
7 weeks ago, by wenzelm
clarified group (but hard to tell);
7 weeks ago, by wenzelm
more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
7 weeks ago, by wenzelm
more lemmas
7 weeks ago, by haftmann
clarified package name (actually both pxfonts and txfonts exist and have this font);
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
prefer isabelle bbbfont;
7 weeks ago, by wenzelm
enforce full build;
7 weeks ago, by wenzelm
clarified symbol names, notably relevant for Z_Notation;
7 weeks ago, by wenzelm
update README (actually after update of component);
7 weeks ago, by wenzelm
high-quality blackboard-bold fonts from "txmia" (package "txfonts");
7 weeks ago, by wenzelm
publish component;
7 weeks ago, by wenzelm
further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
7 weeks ago, by wenzelm
clarified \<Zcomp> (small) vs. \<Zsemi> (big);
7 weeks ago, by wenzelm
more CONTRIBUTORS;
7 weeks ago, by wenzelm
more Z_Notation symbols, as proposed by Simon Foster;
7 weeks ago, by wenzelm
more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus";
7 weeks ago, by wenzelm
clarified order for GUI panel;
7 weeks ago, by wenzelm
prefer more direct interpretation
7 weeks ago, by haftmann
more Z_Notation symbols, as proposed by Simon Foster;
7 weeks ago, by wenzelm
more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt;
7 weeks ago, by wenzelm
clarified order for presentation in isar-ref (Appendix B);
7 weeks ago, by wenzelm
prefer explicit \<Zproject> (with its own Unicode codepoint);
7 weeks ago, by wenzelm
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
7 weeks ago, by wenzelm
tuned message;
7 weeks ago, by wenzelm
proper directory of settings file;
7 weeks ago, by wenzelm
tuned lemma
7 weeks ago, by nipkow
added lemma
7 weeks ago, by nipkow
tuned signature;
8 weeks ago, by wenzelm
tuned signature (again);
8 weeks ago, by wenzelm
tuned --- following hints by IntelliJ;
8 weeks ago, by wenzelm
tuned comments;
8 weeks ago, by wenzelm
proper shell quote;
8 weeks ago, by wenzelm
removed spurious references to perl / libwww-perl;
8 weeks ago, by wenzelm
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
8 weeks ago, by wenzelm
clarified signature: refer to file name instead of file content;
8 weeks ago, by wenzelm
compile;
8 weeks ago, by wenzelm
clarified signature: more explicit types;
8 weeks ago, by wenzelm
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
8 weeks ago, by wenzelm
clarified signature;
8 weeks ago, by wenzelm
elapsed time to download content (and for the server to provide content);
8 weeks ago, by wenzelm
more direct elapsed run_time via bash_process wrapper (via Scala and C);
8 weeks ago, by wenzelm
merged
8 weeks ago, by wenzelm
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
8 weeks ago, by wenzelm
clarified signature: let Sledgehammer handle SystemOnTPTP comments;
8 weeks ago, by wenzelm
clarified signature: url may change dynamically and is part of result;
8 weeks ago, by wenzelm
clarified error;
8 weeks ago, by wenzelm
support timeout, similar to perl LWP::UserAgent;
8 weeks ago, by wenzelm
clarified signature;
8 weeks ago, by wenzelm
tuned;
8 weeks ago, by wenzelm
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
8 weeks ago, by wenzelm
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
8 weeks ago, by wenzelm
clarified HTTP.Content: support encoding;
8 weeks ago, by wenzelm
clarified signature: more explicit HTTP operations;
8 weeks ago, by wenzelm
tuned;
8 weeks ago, by wenzelm
more robust;
8 weeks ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified components;
2 months ago, by wenzelm
avoid name clash
2 months ago, by haftmann
lemma
2 months ago, by haftmann
tuned;
2 months ago, by wenzelm
another example for lift_bnf for quotients
2 months ago, by traytel
merged
2 months ago, by wenzelm
proper \usepackage[T1]{fontenc};
2 months ago, by wenzelm
more robust init: avoid spilling opam artifacts;
2 months ago, by wenzelm
proper type-setting of cartouches (requires T1);
2 months ago, by wenzelm
provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;
2 months ago, by wenzelm
more robust;
2 months ago, by wenzelm
removed unused latex packages;
2 months ago, by wenzelm
obsolete (see 0c837beeb5e7);
2 months ago, by wenzelm
proper Isabelle/Scala tool --- avoid perl;
2 months ago, by wenzelm
generalized confluence-based subdistributivity theorem for quotients;
2 months ago, by traytel
Backed out changeset 3fdb94d87e0e
2 months ago, by desharna
Backed out changeset b867b436f372
2 months ago, by desharna
reduced dependencies on List_Permutation
2 months ago, by haftmann
follow corresponding precedence on sets
2 months ago, by haftmann
consolidated names
2 months ago, by haftmann
reduced dependencies on theory List_Permutation
2 months ago, by haftmann
obsolete (see f3378101f555);
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
more direct unlimited smt_timeout;
2 months ago, by wenzelm
clarified smt: support Timeout.ignored and Timeout.scale_time;
2 months ago, by wenzelm
clarified timeouts in Isabelle/ML;
2 months ago, by wenzelm
tuned --- more elementary Time operations;
2 months ago, by wenzelm
removed unused/pointless operation: Time.start is the load/init time of this Scala module;
2 months ago, by wenzelm
obsolete;
2 months ago, by wenzelm
clarified signature --- augment existing structure Time;
2 months ago, by wenzelm
rebuild SMT certificates from scratch;
2 months ago, by wenzelm
added lemmas (sublist|prefix|suffix)_list_all
2 months ago, by desharna
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While
2 months ago, by desharna
added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI
2 months ago, by desharna
typo
2 months ago, by haftmann
merged
2 months ago, by desharna
added upper bound on monomorphisation duplicate instances
2 months ago, by desharna
tuned best_slices in atp_config
2 months ago, by desharna
tuned exec field in atp_config
2 months ago, by desharna
removed junk;
2 months ago, by wenzelm
tuned proofs;
2 months ago, by wenzelm
enforce full build, after significant changes in Isabelle/Scala;
2 months ago, by wenzelm
clarified compiler options: show relevant warnings;
2 months ago, by wenzelm
tuned --- avoid compiler warnings;
2 months ago, by wenzelm
clarified signature --- fewer warnings;
2 months ago, by wenzelm
clarified signature --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
more robust ordering (see also 88c96e836ed6);
2 months ago, by wenzelm
proper scala.collection.immutable;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
more robust error;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
updated to scala-2.13.5 (with scala-swing_2.13-3.0.0);
2 months ago, by wenzelm
slightly more efficient Term.fastype_of (only little impact in regular applications);
2 months ago, by wenzelm
reduced dependencies on theory List_Permutation
2 months ago, by haftmann
Merge
2 months ago, by paulson
reverted simprule status on a new lemma
2 months ago, by paulson
merged
2 months ago, by paulson
tiny bit of lemma hacking
2 months ago, by paulson
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- avoid deprecated conversions between certain number type;
2 months ago, by wenzelm
tuned --- avoid deprecated Predef.any2stringadd;
2 months ago, by wenzelm
tuned --- silence odd warning;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
tuned --- fewer warnings;
2 months ago, by wenzelm
clarified signature, according to Isabelle/Scala;
2 months ago, by wenzelm
download more directly, via means of JVM;
2 months ago, by wenzelm
download on separate thread;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
NEWS
2 months ago, by haftmann
lemma diffusion
2 months ago, by haftmann
more connections between mset _ = mset _ and permutations
2 months ago, by haftmann
dissolve theory with duplicated name from afp
2 months ago, by haftmann
more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
2 months ago, by wenzelm
more Isabelle/ML/Scala operations;
2 months ago, by wenzelm
more Isabelle/ML/Scala operations;
2 months ago, by wenzelm
more Isabelle/ML/Scala operations;
2 months ago, by wenzelm
proper src1, amending 20157c8ab3f3;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
proper File.eq, amending df49ca5da9d0;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified modules: more like ML;
2 months ago, by wenzelm
obsolete;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
2 months ago, by wenzelm
discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working;
2 months ago, by wenzelm
more checks;
2 months ago, by wenzelm
clarified message;
2 months ago, by wenzelm
clarified message;
2 months ago, by wenzelm
clarified comments;
2 months ago, by wenzelm
clarified message;
2 months ago, by wenzelm
improved list_neq simproc
2 months ago, by nipkow
merged
2 months ago, by haftmann
repaired document
2 months ago, by haftmann
merged
2 months ago, by paulson
merged
2 months ago, by paulson
A couple of basic lemmas about arg
2 months ago, by paulson
multiset as equivalence class of permuted lists
2 months ago, by haftmann
emphasize connection to multisets
2 months ago, by haftmann
proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work;
2 months ago, by wenzelm
more on Isabelle_System.bash;
2 months ago, by wenzelm
more specific name
2 months ago, by haftmann
more lemmas
2 months ago, by haftmann
dropped obscure FIXME
2 months ago, by haftmann
proper usage of hypotheses for zipperposition's TPTP generation
2 months ago, by desharna
merged
2 months ago, by desharna
tuned Mirabelle to parse option check_trivial only once
2 months ago, by desharna
merged
2 months ago, by desharna
merged
2 months ago, by desharna
added stride option to Mirabelle
2 months ago, by desharna
proper prover capabilities for zipperposition
2 months ago, by desharna
NEWS;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
clarified uses of Isabelle_System.bash_process: more checks, fewer messages;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more direct timing from bash_process wrapper;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature, following Isabelle/Scala;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;
2 months ago, by wenzelm
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature, following Isabelle/Scala;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature: process_result timing from Isabelle/Scala;
2 months ago, by wenzelm
NEWS
2 months ago, by haftmann
dedicated locale for preorder and abstract bdd operation
2 months ago, by haftmann
get rid of traditional predicate
2 months ago, by haftmann
proper treatment of process_result;
2 months ago, by wenzelm
more accurate process_result in ML, corresponding to Process_Result in Scala;
2 months ago, by wenzelm
clarified: proper trim_line for error;
2 months ago, by wenzelm
unused;
2 months ago, by wenzelm
clarified lines (again);
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
more uniform Bash.process: always ask Isabelle/Scala;
2 months ago, by wenzelm
more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process);
2 months ago, by wenzelm
clarified compiler options;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
removed obsolete RC tags;
2 months ago, by wenzelm
more hints;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
Added tag Isabelle2021 for changeset 7e2a9a8c2b85
2 months ago, by wenzelm
provide naproche-755224402e36; Isabelle2021
2 months ago, by wenzelm
provide naproche-4ad61140062f;
2 months ago, by wenzelm
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
2 months ago, by Manuel Eberl
tidied up a few ugly proofs
2 months ago, by paulson
merged
2 months ago, by wenzelm
provide naproche-6d0d76ce2f2a;
2 months ago, by wenzelm
Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b
2 months ago, by wenzelm
updated to flatlaf-1.0;
2 months ago, by wenzelm
tuned NEWS;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
3 months ago, by wenzelm
more parallelism: avoid exhaustion of standard thread pool;
3 months ago, by wenzelm
more robust: resolve historic components via current tool to access current server;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more parallelism;
2 months ago, by wenzelm
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
merged;
3 months ago, by wenzelm
Added tag Isabelle2021-RC5 for changeset a88dbf2a020f
3 months ago, by wenzelm
provide naproche-7d0947a91dd5;
3 months ago, by wenzelm
more complete solutions (amending 4d36070bdbf4);
3 months ago, by wenzelm
terminate faster (following dd9fc8a3036c);
3 months ago, by wenzelm
more robust: accommodate output lines produced by Scala "bash_process";
3 months ago, by wenzelm
updated for release;
3 months ago, by wenzelm
updated to flatlaf-1.0-rc3;
3 months ago, by wenzelm
more robust: allow YXML text;
3 months ago, by wenzelm
inherit ISABELLE_TMP from ML process, e.g. required for $AFP/Hello_World/RunningCodeFromIsabelle.thy;
3 months ago, by wenzelm
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
3 months ago, by wenzelm
clarified modules: less redundancy;
3 months ago, by wenzelm
clarified modules: allow early invocation of Scala functions;
3 months ago, by wenzelm
clarified modules: allow early definition of protocol commands;
3 months ago, by wenzelm
clarified links to external files, e.g. .pdf within .thy source document;
3 months ago, by wenzelm
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
3 months ago, by wenzelm
updated to flatlaf-1.0-rc2;
3 months ago, by wenzelm
added lemmas
3 months ago, by nipkow
merged
3 months ago, by wenzelm
updated for release;
3 months ago, by wenzelm
Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb
3 months ago, by wenzelm
provide naproche-20210201;
3 months ago, by wenzelm
clarified messages;
3 months ago, by wenzelm
more parallel;
3 months ago, by wenzelm
more parallel;
3 months ago, by wenzelm
contributors
3 months ago, by Andreas Lochbihler
hide the internal abbreviations MR and MB
3 months ago, by Andreas Lochbihler
optimize RBT_Impl
3 months ago, by mraszyk
merged
3 months ago, by wenzelm
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
3 months ago, by wenzelm
tuned signature: more types;
3 months ago, by wenzelm
clarified signature: proper order;
3 months ago, by wenzelm
clarified signature: more explicit types;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature: no symbol markup within XML attributes;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
bundle more libraries from scala-2.12.x, notably for Isabelle/MMT;
3 months ago, by wenzelm
provide naproche-20210129;
3 months ago, by wenzelm
more robust type signatures, notably for the sake of haskell-stack-trace-plugin-0.1.1.1;
3 months ago, by wenzelm
tuned signature (e.g. see HTML.control_block in Isabelle/Scala);
3 months ago, by wenzelm
proper Isabelle environment (amending 31fbde3baa97);
3 months ago, by wenzelm
updated to jdk-15.0.2+7;
3 months ago, by wenzelm
follow Phabricator update 2021 Week 4;
3 months ago, by wenzelm
more NEWS;
3 months ago, by wenzelm
more uniform directory layout for macOS;
3 months ago, by wenzelm
more generic Isabelle_app;
3 months ago, by wenzelm
prefer dynamic linking: platform is always x86_64 (see 373dcdd363dc);
3 months ago, by wenzelm
more robust;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
provide jdk-11.0.10+9.tar.gz LTS for testing (inactive);
3 months ago, by wenzelm
Simpler proof
3 months ago, by nipkow
more robust: support other_isabelle.init_settings for build_history before b93404a4c3dd;
3 months ago, by wenzelm
more robust: defer error in sessions structure to build process;
3 months ago, by wenzelm
merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS;
3 months ago, by wenzelm
Added tag Isabelle2021-RC3 for changeset 02422c9add5e
3 months ago, by wenzelm