- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Sep 7 2022
Sep 7 2022
desharna committed rISABELLEa4b47c684445: moved mono and strict_mono to Fun and redefined them as abbreviations.
moved mono and strict_mono to Fun and redefined them as abbreviations
desharna committed rISABELLE8d56461f85ec: moved antimono to Fun and redefined it as an abbreviation.
moved antimono to Fun and redefined it as an abbreviation
Sep 5 2022
Sep 5 2022
clarified generic euclidean relation
blanchette committed rISABELLE6a20d0ebd5b3: added a bound in SMT on the number of schematic constants considered -- the….
added a bound in SMT on the number of schematic constants considered -- the…
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFPff719c05809a: Updated citations.
Updated citations
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFP73f15452e56f: Updated citations.
Updated citations
Sep 3 2022
Sep 3 2022
makarius committed rISABELLEf1dc3d9d5164: check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library..
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.
tuned --- more robust syntax;
makarius committed rISABELLE507c65cc4332: back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant….
back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant…
unused (see 347ed6219dab);
Christian Urban <christian.urban@kcl.ac.uk> committed rAFP14eb275d680e: merged.
merged
Christian Urban <christian.urban@kcl.ac.uk> committed rAFPf294e5dddd66: Substantial additions by Franz Regensburger to the Universal_Turing_Machine….
Substantial additions by Franz Regensburger to the Universal_Turing_Machine…
tuned timeouts, based on test runs with threads=1;
more CONTRIBUTORS + NEWS;
proper description;
Norbert Schirmer <nschirmer@apple.com> committed rISABELLEca7737249aa4: option "sort_updates" for record update simproc. Make proper record simproc….
option "sort_updates" for record update simproc. Make proper record simproc…
Sep 2 2022
Sep 2 2022
replaced slow smt call by blast
Sep 1 2022
Sep 1 2022
paulson <lp15@cam.ac.uk> committed rISABELLEf3f1cf4711d7: Three new theorems about real polynomial functions.
Three new theorems about real polynomial functions
clarified GUI behaviour;
Aug 31 2022
Aug 31 2022
eliminated odd Unicode blanks;
eliminated DOS line endings;
eliminated tabs, assuming tab-width=8;
eliminated tabs, assuming tab-width=4;
updated to current Cygwin, near 3.3.5-1;
test macOS 12 Monterey via laramac01;
clarified GUI update;
clarified signature;
more GUI functionality;
makarius committed rISABELLE752425c69577: clarified component structure, concerning initialization order;.
clarified component structure, concerning initialization order;
clarified signature;
avoid hardwired document;
Aug 30 2022
Aug 30 2022
makarius committed rISABELLE04ce6cf2bd3b: update VSCodium 1.65.2 ~> 1.70.1, Electron 13.5.2 ~> 18.3.5, Node.js v14.16.0….
update VSCodium 1.65.2 ~> 1.70.1, Electron 13.5.2 ~> 18.3.5, Node.js v14.16.0…
Aug 29 2022
Aug 29 2022
provide cvc5-1.0.2 (inactive);
tool to build Isabelle component for cvc5;
tuned: avoid odd stateful programming;
replace smt_oracle by proper veriT reconstruction
Aug 28 2022
Aug 28 2022
more markup (for batch build);
updated some links;
makarius committed rISABELLEadf9c4d68581: more links, for files that formally belong to this session;.
more links, for files that formally belong to this session;
tuned antiquotations;
Aug 27 2022
Aug 27 2022
makarius updated the post content for Blog Post: Session ROOT files support 'chapter_definition' entries.
make all sessions of chapter "AFP" belong to group "AFP";
makarius committed rISABELLEc9d56340b56e: ZF belongs to chapter FOL, following lib/html/library_index_content.template (i..
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.
makarius committed rISABELLEa9bbf075f431: include groups from 'chapter_definition' in session info, based on the state of….
include groups from 'chapter_definition' in session info, based on the state of…
makarius committed rISABELLE152c5c83c119: proper chapter_definition to prevent odd definitions by users;.
proper chapter_definition to prevent odd definitions by users;
chapter_definition for presentation;
tuned whitespace for presentation;
clarified syntax: more uniform;
makarius committed rISABELLEb831a0bdd751: clarified signature of Sessions.Session: chapter_defs: vs. known_chapters (in….
clarified signature of Sessions.Session: chapter_defs: vs. known_chapters (in…
more robust, more strict;
Aug 26 2022
Aug 26 2022
clarified chapters: de-emphasize minor examples;
clarified signature;
makarius committed rISABELLE46c6f649a943: produce root index based on sessions_structure.chapter_defs;.
produce root index based on sessions_structure.chapter_defs;
makarius committed rISABELLEca73ced9e630: provide chapter descriptions, based on lib/html/library_index_content.template;.
provide chapter descriptions, based on lib/html/library_index_content.template;
more robust: proper system_name;
makarius committed rISABELLE27d98da31985: support 'chapter_definition' with description for presentation purposes;.
support 'chapter_definition' with description for presentation purposes;
makarius committed rISABELLE34dd96a06c45: removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g..
removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g.
makarius committed rISABELLE2fff9ce6b460: more aggressive clean_directory(session_dir), while rm_tree is guarded by….
more aggressive clean_directory(session_dir), while rm_tree is guarded by…
clarified signature;
clarified signature;
makarius committed rISABELLE59aa034220bf: more robust: ensure that chapter/session/theory do not contain special notation….
more robust: ensure that chapter/session/theory do not contain special notation…
paulson <lp15@cam.ac.uk> committed rISABELLE44e0ba464e08: NEWS about Sum_of_Powers.
NEWS about Sum_of_Powers