testboard: Graph

added lemmas filter_mset_cong{0,} draft default tip
46 hours ago, by desharna
tidied auto / simp with null arguments
4 days ago, by paulson
tuned signature;
10 days ago, by wenzelm
provide Isabelle/Electron test;
10 days ago, by wenzelm
tuned text;
12 days ago, by wenzelm
tuned text;
12 days ago, by wenzelm
Tidied up some super-messy proofs
2 weeks ago, by paulson
added lemmas image_mset_image_mset_mem_multI and multp_image_mset_image_msetI draft
5 days ago, by desharna
added lemma image_mset_image_mset_mem_multI from AFP/SuperCalc draft
5 days ago, by desharna
Added a couple of obvious simprules
2 weeks ago, by paulson
added lemma
2 weeks ago, by nipkow
tuned signature: avoid problems with scala3;
4 weeks ago, by wenzelm
proper indentation;
4 weeks ago, by wenzelm
merged
4 weeks ago, by wenzelm
clarified management of interpreter threads: more generic;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
clarified signature, based on hints by IntelliJ IDEA;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
more robust: avoid partiality;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
tuned --- avoid warnings in scala3;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
pass new option only to new version of E
5 weeks ago, by blanchet
merged
5 weeks ago, by desharna
merged
6 weeks ago, by wenzelm
revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
6 weeks ago, by wenzelm
merged
6 weeks ago, by wenzelm
tuned --- avoid warnings in scala3;
6 weeks ago, by wenzelm
tuned --- avoid redundant patterns;
6 weeks ago, by wenzelm
avoid pattern-match warnings, notably in scala3;
6 weeks ago, by wenzelm
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;
6 weeks ago, by wenzelm
tuned --- accomodate scala3;
6 weeks ago, by wenzelm
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;
6 weeks ago, by wenzelm
back to more ambitious scala-3.1.1 (see 8b7497992301);
6 weeks ago, by wenzelm
tuned --- fewer warnings in scala3;
6 weeks ago, by wenzelm
tuned -- avoid warnings for scala3;
6 weeks ago, by wenzelm
tuned signature -- avoid warnings for scala3;
6 weeks ago, by wenzelm
removed unused flag (see 25c6423ec538);
6 weeks ago, by wenzelm
clarified versions;
6 weeks ago, by wenzelm
documentation on diagnostic devices for code generation
6 weeks ago, by haftmann
more correct language
6 weeks ago, by haftmann
enable an E option suggested by Petar Vukmirovic
6 weeks ago, by blanchet
reused slice in Sledgehammer's minimizer
6 weeks ago, by desharna
used HTTPS for SystemOnTPTP
6 weeks ago, by desharna
moved from AFP to distribution
6 weeks ago, by haftmann
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
6 weeks ago, by wenzelm
more operations;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
tuned: avoid ambiguity in scala3;
6 weeks ago, by wenzelm
clarified signature: avoid ambiguity in scala3;
6 weeks ago, by wenzelm
clarified signature: avoid ambiguity in scala3;
6 weeks ago, by wenzelm
more robust types (for scala3);
6 weeks ago, by wenzelm
tuned for scala3;
6 weeks ago, by wenzelm
proper indentation (relevant for scala3);
6 weeks ago, by wenzelm
adjusted printing of type annotations to accomodate Scala 3
6 weeks ago, by haftmann
two new examples
6 weeks ago, by paulson
pass constructor arity as part of case certficiate
7 weeks ago, by haftmann
tuned whitespace in generated code
7 weeks ago, by haftmann
tuned, centralizing case distinction at one place at the cost of modest duplication
7 weeks ago, by haftmann
clarified formatting, for the sake of scala3;
7 weeks ago, by wenzelm
merged
7 weeks ago, by wenzelm
tuned formatting;
7 weeks ago, by wenzelm
clarified formatting, for the sake of scala3;
7 weeks ago, by wenzelm
tuned
7 weeks ago, by haftmann
tuned
7 weeks ago, by haftmann
merge
7 weeks ago, by blanchet
tuned slices to get the fifth Zipperposition slice in a typical run
7 weeks ago, by blanchet
merged
7 weeks ago, by desharna
tuned spelling;
7 weeks ago, by wenzelm
merged
7 weeks ago, by wenzelm
updated to scala-parser-combinators 2.1.0, which also fits to scala-3.0.2;
7 weeks ago, by wenzelm
clarified invocation of isabelle.setup.Setup: -classpath allows multiple jars, as required for scala3;
7 weeks ago, by wenzelm
tuned: eliminted do-while for the sake of scala3;
7 weeks ago, by wenzelm
prefer scala 3.0.x, for option "-source 3.0-migration";
7 weeks ago, by wenzelm
tuned: avoid problems with scala3;
7 weeks ago, by wenzelm
tuned: avoid problems with scala3;
7 weeks ago, by wenzelm
provide SCALA_INTERFACES for isabelle_setup;
7 weeks ago, by wenzelm
build Isabelle Scala component from official downloads (for scala-3.1.1);
8 weeks ago, by wenzelm
tuned sledgehammer documentation
7 weeks ago, by desharna
added documentation
7 weeks ago, by desharna
merged
7 weeks ago, by desharna
further tweaked E's setup
7 weeks ago, by blanchet
tweaked E setup
7 weeks ago, by blanchet
merged
7 weeks ago, by desharna
NEWS and CONTRIBUTORS
7 weeks ago, by haftmann
nicer TPTP output
7 weeks ago, by blanchet
tuned sledehammer to return best succeeding preplay method
7 weeks ago, by desharna
expanded sledgehammer's expect option with some_preplayed
7 weeks ago, by desharna
added preplay results to sledgehammer_output
7 weeks ago, by desharna
tuned sledgehammer to suggest (smt (verit)) on failing smt preplay for all but Z3
7 weeks ago, by desharna
expanded sledgehammer's expect option with some_preplayed draft
7 weeks ago, by desharna
changed sledgehammer_output draft
7 weeks ago, by desharna
post-merged into new Lethe code
7 weeks ago, by desharna
merged
7 weeks ago, by desharna
regenerated
7 weeks ago, by haftmann
tighter check to ensure that patterns remain left-linear, previous implementation was overcautious
7 weeks ago, by haftmann
tuned
7 weeks ago, by haftmann
tuned
7 weeks ago, by haftmann
separated treatment of undefined bodys
7 weeks ago, by haftmann
tuned arguments
7 weeks ago, by haftmann
modernized handling of variables
7 weeks ago, by haftmann
fixed generation of Isar proofs e89709b80b6e
7 weeks ago, by desharna
fixed Sledgehammer generation of Isar proofs for SMT solvers broken by e89709b80b6e draft
7 weeks ago, by desharna
structurally tuned
7 weeks ago, by haftmann
tuned names
7 weeks ago, by haftmann
prefer build combinator
7 weeks ago, by haftmann
tuned whitespace
7 weeks ago, by haftmann
proper option argument;
8 weeks ago, by wenzelm
prefer Isabelle shasum over the old command-line tool with its extra marker character;
8 weeks ago, by wenzelm
tuned signature;
8 weeks ago, by wenzelm
tuned signature;
8 weeks ago, by wenzelm
tuned text, without update of component for now;
8 weeks ago, by wenzelm
omit somewhat pointless integrity check;
8 weeks ago, by wenzelm
tuned;
8 weeks ago, by wenzelm
compile TPTP module
8 weeks ago, by blanchet
compile mirabelle
8 weeks ago, by blanchet
further modernized E setup
8 weeks ago, by blanchet
cleaned up obsolete E setup and a bit of SPASS
8 weeks ago, by blanchet
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
8 weeks ago, by blanchet
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
8 weeks ago, by blanchet
updated vscode_extension;
8 weeks ago, by wenzelm
added parentheses in TPTP output -- seem necessary for some provers
8 weeks ago, by blanchet
merged
8 weeks ago, by wenzelm
provide pre-built vscodium-1.65.2 for all platforms;
8 weeks ago, by wenzelm
tuned;
8 weeks ago, by wenzelm
provide vscode_extension via component, thus users don't need Node.js development tools;
8 weeks ago, by wenzelm
clarified options;
8 weeks ago, by wenzelm
Some new library lemmas
8 weeks ago, by paulson
merged
8 weeks ago, by paulson
tuned
8 weeks ago, by haftmann
separated case reduction
8 weeks ago, by haftmann
separated selector function entirely
8 weeks ago, by haftmann
self-contained extraction auf clauses
8 weeks ago, by haftmann
extracted selector function, restoring code generation for let expressions
8 weeks ago, by haftmann
streamlined
8 weeks ago, by haftmann
streamlined
8 weeks ago, by haftmann
streamlined
8 weeks ago, by haftmann
disentangled
8 weeks ago, by haftmann
really removing Dedekind_real
8 weeks ago, by paulson
merged
8 weeks ago, by paulson
merged
8 weeks ago, by wenzelm
tuned message;
8 weeks ago, by wenzelm
more operations;
8 weeks ago, by wenzelm
tuned signature;
8 weeks ago, by wenzelm
more robust install/uninstall;
8 weeks ago, by wenzelm
more formal extension_manifest, with shasum for sources;
8 weeks ago, by wenzelm
tuned;
8 weeks ago, by wenzelm
tuned signature;
8 weeks ago, by wenzelm
clarified signature;
8 weeks ago, by wenzelm
proper usage;
8 weeks ago, by wenzelm
tuned -- follow sha1_digest in src/Tools/Setup/src/Build.java;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
... and removing Primrec from ROOT too
8 weeks ago, by paulson
Removal of the Primrec example in preparation for making it an AFP entry
8 weeks ago, by paulson
merged
8 weeks ago, by desharna
split veriT reconstruction into Lethe and veriT part
2 months ago, by Mathias Fleury
clarified options;
2 months ago, by wenzelm
more robust errors -- on foreground process instead of background server;
2 months ago, by wenzelm
clarified options -l vs. -R;
2 months ago, by wenzelm
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
2 months ago, by wenzelm
proper command-line tool;
2 months ago, by wenzelm
support console output, e.g. "isabelle vscode -C -- --help";
2 months ago, by wenzelm
run Isabelle/VSCode via Scala;
2 months ago, by wenzelm
clarified module name;
2 months ago, by wenzelm
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
2 months ago, by wenzelm
incorporate build_grammar into build_vscode_extension;
2 months ago, by wenzelm
removed old generated file;
2 months ago, by wenzelm
Moving Dedekind_Real to the AFP
8 weeks ago, by paulson
avoided recomputation in Cooper.djf and ran `isabelle regenerate_cooper`
2 months ago, by desharna
split veriT reconstruction into Lethe and veriT part draft
2 months ago, by Mathias Fleury
Tidied several ugly proofs in some elderly examples
2 months ago, by paulson
tuned message;
2 months ago, by wenzelm
clarified errors;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
support Node.js as well, reusing the engine from Electron/VSCodium;
2 months ago, by wenzelm
updated to vscode 1.65.2;
2 months ago, by wenzelm
proper result check;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
clarified directory layout and settings: more robust on all platforms;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
support Electron application framework;
2 months ago, by wenzelm
generated lemma map_ident_strong for BNFs
2 months ago, by desharna
updated SMT certificates
2 months ago, by desharna
generated lemma map_ident_strong for BNFs draft
2 months ago, by desharna
generated lemma map_ident_strong for BNFs draft
2 months ago, by desharna
updated SMT certificates draft
2 months ago, by desharna
used more descriptive assert names in SMT-Lib output
2 months ago, by desharna
clarified and unified executable names;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode;
2 months ago, by wenzelm
fix handling of lambdas in reconstruction of eq_congruent
2 months ago, by Mathias Fleury
more robust: avoid breakdown of Search dialog;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
always use Isabelle encoding, as in Isabelle/jEdit;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature: more uniform ts vs. Scala;
2 months ago, by wenzelm
discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
2 months ago, by wenzelm
generated lemma map_ident_strong for BNFs draft
2 months ago, by desharna
fix handling of lambdas in reconstruction of eq_congruent draft
2 months ago, by Mathias Fleury
actually decode/encode symbols;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
prefer yarn over npm;
2 months ago, by wenzelm
more accurate .hgignore;
2 months ago, by wenzelm
clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
proper init_resources for macos;
2 months ago, by wenzelm
clarified names;
2 months ago, by wenzelm
clarified modules: vscode vs. extension;
2 months ago, by wenzelm
inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
patch VSCode source tree to support isabelle_encoding.ts;
2 months ago, by wenzelm
more robust, pass "yarn valid-layers-check";
2 months ago, by wenzelm
clarified directories;
2 months ago, by wenzelm
patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet;
2 months ago, by wenzelm
fit into vscode source conventions;
2 months ago, by wenzelm
A tiny further cleanup
2 months ago, by paulson
used more descriptive assert names in SMT-Lib output draft
2 months ago, by desharna
used more descriptive assert names in SMT-Lib output draft
2 months ago, by desharna
used more descriptive assert names in SMT-Lib output draft
2 months ago, by desharna
Tidied some messy proofs
2 months ago, by paulson
merged
2 months ago, by nipkow
towards UTF-8-Isabelle symbol encoding;
2 months ago, by wenzelm
updated to VSCode 1.65.0;
2 months ago, by wenzelm
clarified char symbols: cover most European languages;
2 months ago, by wenzelm
more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
more count_list lemmas
2 months ago, by nipkow
more robust dependencies: avoid implicit update, escpecially of underlying vscode engine;
2 months ago, by wenzelm
proper file headers;
2 months ago, by wenzelm
added count_list lemmas
2 months ago, by nipkow
tuned message;
2 months ago, by wenzelm
more compact result;
2 months ago, by wenzelm