- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Aug 4 2021
Aug 4 2021
desharna committed rISABELLEed1f576df9c4: added dummy_thf prover to Sledgehammer.
added dummy_thf prover to Sledgehammer
Aug 3 2021
Aug 3 2021
florian.haftmann committed rAFP13152a0c7b0c: simplified hierarchy of type classes for bit operations.
simplified hierarchy of type classes for bit operations
florian.haftmann committed rISABELLE3146646a43a7: simplified hierarchy of type classes for bit operations.
simplified hierarchy of type classes for bit operations
makarius committed rISABELLE4984fad0e91d: more operations, notably free and bound variables as in Isabelle/Pure;.
more operations, notably free and bound variables as in Isabelle/Pure;
Aug 2 2021
Aug 2 2021
restored executable conversions
more operations on types and terms;
clarified jEdit java sources;
makarius committed rISABELLE3b56d00ac333: clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for….
clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for…
moved theory Bit_Operations into Main corpus
moved theory Bit_Operations into Main corpus
Aug 1 2021
Aug 1 2021
clarified signature;
clarified signature;
organize syntax for word operations in bundles
organize syntax for word operations in bundles
Jul 31 2021
Jul 31 2021
support for Lazy.Text;
prefer compact Isabelle.Bytes;
clarified signature;
clarified signature --- more operations;
clarified order of modules;
more systematic approach for instantiation
avoid seemingly unused transfer rules
Jul 30 2021
Jul 30 2021
clarified signature;
clarified signature;
prefer Isabelle.Bytes, based on ShortByteString;
tuned signature: more generic operations;
makarius committed rISABELLE5b68a5cd7061: prefer UTF8 implementation from Data.Text.Encoding (foreign C);.
prefer UTF8 implementation from Data.Text.Encoding (foreign C);
yonoteam committed rAFP6beec57f7d3f: cleaner presentation of analysis theorems in preliminaries.
cleaner presentation of analysis theorems in preliminaries
Jul 29 2021
Jul 29 2021
Asta Halkjær From <andro.from@gmail.com> committed rAFPe1046d8be835: Update to new Epistemic_Logic.thy.
Update to new Epistemic_Logic.thy
Asta Halkjær From <andro.from@gmail.com> committed rAFP09d0f0e8b5f5: Avoid typedefs.
Avoid typedefs
desharna committed rISABELLE180ee02eb075: documented Mirabelle_Sledgehammer's new keep semantics.
documented Mirabelle_Sledgehammer's new keep semantics
desharna committed rISABELLEa2cbe81e1e32: changed Mirabelle_Sledgehammer keep option from path to boolean.
changed Mirabelle_Sledgehammer keep option from path to boolean
Jul 28 2021
Jul 28 2021
desharna committed rISABELLEb93d8c2ebab0: added automatic uniform stride option to Mirabelle.
added automatic uniform stride option to Mirabelle
desharna committed rISABELLE97ad1687cec7: fixed HOL-ex following a5bab59d580b.
fixed HOL-ex following a5bab59d580b
desharna committed rISABELLEa5bab59d580b: added support for TFX $let to Sledgehammer's TPTP output.
added support for TFX $let to Sledgehammer's TPTP output
Jul 27 2021
Jul 27 2021
desharna committed rISABELLE6c8473b4f518: fixed TFX generation when universal quantifier is used as term.
fixed TFX generation when universal quantifier is used as term
support for native symlinks on Windows;
various improvements of "isabelle scala_project";
desharna committed rISABELLEffbd1b7e5439: tuned Mirabelle's theory selection.
tuned Mirabelle's theory selection
Clean: set AFP standard document options
Clean: re-add to chapter AFP
paulson <lp15@cam.ac.uk> committed rAFP62ea872d1534: Finitely_Generated_Abelian_Groups website.
Finitely_Generated_Abelian_Groups website
paulson <lp15@cam.ac.uk> committed rAFP6f6a17c6bdde: new entry Finitely_Generated_Abelian_Groups.
new entry Finitely_Generated_Abelian_Groups
Jul 26 2021
Jul 26 2021
Added Finitely_Generated_Abelian_Groups to metadata
clarified signature;
clarified signature;
Jul 25 2021
Jul 25 2021
updated for Isabelle2021 release;
makarius committed rISABELLEf175fd68b6a9: back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012….
back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012…
clarified version: Apple now counts like 11, 12, ...;
update to Haskell stack-2.7.3 and stackage lts-17.15;
Jul 24 2021
Jul 24 2021
makarius committed rISABELLE203dfa8bc0fc: clarified compiler output: allow multithreaded execution;.
clarified compiler output: allow multithreaded execution;
clarified signature;
clarified signature: more operations;
clarified props: more permissive;
clarified properties: "module" and "no_build";
clarified signature;
clarified signature;
Jul 23 2021
Jul 23 2021
makarius committed rISABELLEf34d54b0e5de: clarified names (again), e.g. relevant for "Plugin Options";.
clarified names (again), e.g. relevant for "Plugin Options";
Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFP49d3aa43c180: Sync with my development repo. Add new material: "concrete bicategories" and.
Sync with my development repo. Add new material: "concrete bicategories" and
Jul 22 2021
Jul 22 2021
desharna committed rISABELLEbd575b1bd9bf: added simp_options to meson.
added simp_options to meson
Jul 19 2021
Jul 19 2021
parse TPTP operator @ also when not parenthesized
tuned E's lambda encoding
removed setup for outdated CVC3 from Isabelle
blanchette committed rISABELLE462d652ad910: use Vampire's clausifier with iProver, now that E's is no longer supported.
use Vampire's clausifier with iProver, now that E's is no longer supported
blanchette committed rISABELLE302994f5a3c2: updated Sledgehammer docs -- removed most version numbers since these are….
updated Sledgehammer docs -- removed most version numbers since these are…
Jul 18 2021
Jul 18 2021
updated documentation on Isabelle/Scala;
makarius committed rISABELLE8c213672f6f3: clarified component setup: exclude jar from active component, but use sources….
clarified component setup: exclude jar from active component, but use sources…
discontinued obsolete Apple (deprecated);
more robust "isabelle build_scala" as separate tool;
Jul 17 2021
Jul 17 2021
tuned --- based on hints by IntelliJ IDEA;
makarius committed rISABELLE57768f30d17c: more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in….
more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in…
more portable across history;
proper isabelle.setup.Setup build;
rebuild component;
makarius committed rISABELLEc9ec6f03ab91: more complete scala_project, including Isabelle/jEdit plugins;.
more complete scala_project, including Isabelle/jEdit plugins;
makarius committed rISABELLE39e05601faeb: more accurate scala_project, based on build.props of components;.
more accurate scala_project, based on build.props of components;
clarified directories;