- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Yesterday
Yesterday
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb48d456f9336: merge.
merge
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP70ac843c069d: increased timeout.
increased timeout
collected combinatorial material
collected combinatorial material
Sat, Apr 10
Sat, Apr 10
more documentation;
proper treatment of nested antiquotations;
makarius committed rISABELLE2f6855142a8c: support for ML special forms: modified evaluation similar to Scheme;.
support for ML special forms: modified evaluation similar to Scheme;
makarius committed rISABELLEa2c589d5e1e4: clarified signature: more detailed token positions for antiquotations;.
clarified signature: more detailed token positions for antiquotations;
Fri, Apr 9
Fri, Apr 9
Asta Halkjær From <andro.from@gmail.com> committed rAFP0fa3d918ef8c: Update root.tex.
Update root.tex
Asta Halkjær From <andro.from@gmail.com> committed rAFP285e1cc62c43: Cut out Fitting's consistency properties.
Cut out Fitting's consistency properties
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPcf0a3199f4e7: fixed proof.
fixed proof
Thu, Apr 8
Thu, Apr 8
clarified message, following Isabelle/a7aabdf889b7;
clarified signature;
florian.haftmann committed rAFPc351b9b63b58: confluent preprocessing for floats in presence of target language numerals.
confluent preprocessing for floats in presence of target language numerals
florian.haftmann committed rISABELLE7cb3fefef79e: confluent preprocessing for floats in presence of target language numerals.
confluent preprocessing for floats in presence of target language numerals
subclass relation
Wed, Apr 7
Wed, Apr 7
some tinkering with npm versions;
some tinkering with npm versions;
back to post-release mode;
auto-update due to "isabelle build_vscode";
tuned --- following hints by IntelliJ IDEA;
pruvisto committed rISABELLE56db8559eadb: fixed problematic addition operation in the 'approximation' package (previous….
fixed problematic addition operation in the 'approximation' package (previous…
adapted to isabelle-dev/56db8559eadb
simplified definition
simplified definition
Tue, Apr 6
Tue, Apr 6
nipkow committed rAFPd552c27edab9: probable fix suggested by Cornelius for the changes in the vicinity of….
probable fix suggested by Cornelius for the changes in the vicinity of…
Mon, Apr 5
Mon, Apr 5
makarius committed rISABELLEe7fb17bca374: discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog….
discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog…
makarius committed rISABELLE543d5539306d: following recent Phabricator update, after 2021 Week 13 (Late March);.
following recent Phabricator update, after 2021 Week 13 (Late March);
Sat, Apr 3
Sat, Apr 3
nipkow committed rAFP9ce1745d994d: Fixes due to new order prover.
Fixes due to new order prover
Fri, Apr 2
Fri, Apr 2
paulson <lp15@cam.ac.uk> committed rISABELLEc89922715bf5: Cosmetic: no !! in the lemma statement.
Cosmetic: no !! in the lemma statement
Thu, Apr 1
Thu, Apr 1
more standard header, with utf-8 encoding;
makarius committed rISABELLEc337c798f64c: clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;.
clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
paulson <lp15@cam.ac.uk> committed rAFP589a6dadfa84: another broken proof.
another broken proof
paulson <lp15@cam.ac.uk> committed rAFP3b2637ae2d8c: Fixed and simplified some failing proofs.
Fixed and simplified some failing proofs
new automatic order prover: stateless, complete, verified
Wed, Mar 31
Wed, Mar 31
clarified signature;
clarified: follow "isabelle version -t";
makarius committed rISABELLE2cd23d587db9: further clarification of Isabelle distribution identification -- avoid odd….
further clarification of Isabelle distribution identification -- avoid odd…
more robust and uniform ISABELLE_TAGS;
tuned signature -- more explicit types;
makarius committed rISABELLE8f485a199874: simplified release status (again), in contrast to a43898f76ae9;.
simplified release status (again), in contrast to a43898f76ae9;
makarius committed rISABELLE4cba4e250c28: clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;.
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
more uniform HTTP resources;
makarius committed rISABELLEd3f2038198ae: clarified (again): local tip could be actually more recent;.
clarified (again): local tip could be actually more recent;
makarius committed rISABELLEb7bb665fe850: more systematic java_library: avoid empty entries, declaration order as for….
more systematic java_library: avoid empty entries, declaration order as for…
paulson <lp15@cam.ac.uk> committed rAFP34dff8ee061c: Writing less_sets as an infix.
Writing less_sets as an infix
Tue, Mar 30
Tue, Mar 30
makarius committed rISABELLEe52a9b208481: support sequential LaTeX jobs: more robust when TeX installation is self….
support sequential LaTeX jobs: more robust when TeX installation is self…
avoid symblinks --- make it work on Windows;
paulson <lp15@cam.ac.uk> committed rAFPb64d3bdac4d9: Fixed some looping proofs (though why they were looping isn't clear).
Fixed some looping proofs (though why they were looping isn't clear)
makarius added a comment to rISABELLE2cdbb6a2f2a7: updated to latest latex due to new mechanism for dealing with bold ccfonts.
See also https://www.texfaq.org/FAQ-concrete
nipkow committed rISABELLE2cdbb6a2f2a7: updated to latest latex due to new mechanism for dealing with bold ccfonts.
updated to latest latex due to new mechanism for dealing with bold ccfonts
Mon, Mar 29
Mon, Mar 29
paulson <lp15@cam.ac.uk> committed rAFP74dd55b9ef33: Fixed a failing proof.
Fixed a failing proof
paulson <lp15@cam.ac.uk> committed rAFP86e8a4b1fb58: fixes for new hd_rev and last_rev.
fixes for new hd_rev and last_rev
paulson <lp15@cam.ac.uk> committed rISABELLEc526eb2c7ca0: removal of needless hypothesis in hd_rev and last_rev.
removal of needless hypothesis in hd_rev and last_rev
paulson <lp15@cam.ac.uk> committed rAFPe928ad3a61c3: Infix notation for the less_sets relation.
Infix notation for the less_sets relation
paulson <lp15@cam.ac.uk> committed rAFPa1f0a543602e: simplified a few proofs.
simplified a few proofs
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP92bb16b93fd2: sitegen and metadata for Constructive_Cryptography_CM.
sitegen and metadata for Constructive_Cryptography_CM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP680fb435498b: new entry Constructive_Cryptography_CM.
new entry Constructive_Cryptography_CM
Sun, Mar 28
Sun, Mar 28
clarified message;
more options: build is part of default setup;
misc tuning and clarification;
proper Admin script, outside the settings environment;
Sat, Mar 27
Sat, Mar 27
more accurate settings after update of current version;
clarified messages;
more robust: lest hg work out remote tip;
makarius committed rISABELLEdbe5bbc2331e: clarified treatment of multiple versions: last one counts;.
clarified treatment of multiple versions: last one counts;
more robust: explicit repository root;
more convenient repository setup;
more robust invocation of hg;