- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Jun 4 2020
Jun 4 2020
activate simproc for FOL
more rules for FOL also
more simp rules
activate simproc for FOL
more rules for FOL also
Jun 3 2020
Jun 3 2020
Asta Halkjær From <s144442@student.dtu.dk> committed rAFP478526986480: Small abstract correction..
Small abstract correction.
Asta Halkjær From <s144442@student.dtu.dk> committed rAFP6ae0a1721dae: Prove completeness of the fully restricted system..
Prove completeness of the fully restricted system.
nipkow committed rISABELLE4c5778d8a53d: should have been copied across from Set.thy as well for better printing.
should have been copied across from Set.thy as well for better printing
May 31 2020
May 31 2020
simplified Let constructor
May 30 2020
May 30 2020
florian.haftmann committed rISABELLE435cdc772110: specific atomization inert to later rule set modifications.
specific atomization inert to later rule set modifications
more precise scope of atomize
install simproc but deactivate by default
May 27 2020
May 27 2020
adapted to d25093536482;
clarified signature;
proper error positions;
more documentation on Isabelle/Scala;
more antiquotations;
makarius committed rISABELLE1529336eaedc: check bash functions against Isabelle settings environment;.
check bash functions against Isabelle settings environment;
breakable scala_name;
proper check of example;
discontinued pointless document antiquotation;
makarius committed rISABELLEce06d6456cc8: clarified signature --- fit within limit of 22 arguments;.
clarified signature --- fit within limit of 22 arguments;
May 25 2020
May 25 2020
more antiquotations;
check free-form Scala source;
clarified static_check: avoid accidental evaluation;
makarius committed rISABELLE8dbefe849666: omit pointless memoing: Scala compiler is rather bulky anyway;.
omit pointless memoing: Scala compiler is rather bulky anyway;
clarified signature;
antiquotations for Scala entities;
more systematic self-citations
better closeup and more consistent terminology
May 24 2020
May 24 2020
proper stack_limit;
clarified signature;
proper check of registered Scala functions;
more accurate classpath for "isabelle scala";
makarius committed rISABELLE0ca353521753: asynchronous build_session: notably for Scala.fulfill protocol commands during….
asynchronous build_session: notably for Scala.fulfill protocol commands during…
clarified build_session protocol;
clarified signature;
more robust: explicit check for PIDE session;
check Scala source snippets from ML;
init default context;
makarius committed rISABELLE28def00726ca: more robust isabelle.Functions --- avoid Java reflection with unclear….
more robust isabelle.Functions --- avoid Java reflection with unclear…
clarified signature;
more brackets (see 2e8af171887f);
clarified signature;
more robust, notably for "isabelle scala";
clarified signature;
nipkow committed rISABELLE86cfb9fa3da8: reorganised sorted_set_of_list.
reorganised sorted_set_of_list
paulson <lp15@cam.ac.uk> committed rISABELLEd73955442df5: a few new lemmas about functions.
a few new lemmas about functions
May 23 2020
May 23 2020
paulson <lp15@cam.ac.uk> committed rAFPda460a208d37: getting rid of inj_on_image_mem_iff_alt.
getting rid of inj_on_image_mem_iff_alt
May 22 2020
May 22 2020
nipkow committed rISABELLEe9df7895e331: comment makes no sense.
comment makes no sense
no need to enforce safety of final interval enclosure
nipkow committed rAFP25ba40a59673: adapted to 3e343c0c2138.
adapted to 3e343c0c2138
recover from unsafe set during Picard iteration
slightly more specific implementations
tuned module name space for generated code
May 21 2020
May 21 2020
paulson <lp15@cam.ac.uk> committed rAFP944409c54399: new theorems, esp. on order types.
new theorems, esp. on order types
generalized and augmented
May 20 2020
May 20 2020
clarified signature;
clarified modules;
paulson <lp15@cam.ac.uk> committed rISABELLE3c7852327787: A few new theorems, plus some tidying up.
A few new theorems, plus some tidying up
corrected spelling and tuned whitespace
May 19 2020
May 19 2020
blanchette committed rAFPc6352b79465d: use lhd and lnull rather than lnth 0 and llength = 0 in IsaFoL.
use lhd and lnull rather than lnth 0 and llength = 0 in IsaFoL
blanchette committed rAFP12e81252fc8d: merged two files that used to be split for technical/political reasons.
merged two files that used to be split for technical/political reasons
more work on liminf llist library
May 18 2020
May 18 2020
enriched theorem proving library
follow Phabricator update 2020 Week 19;
May 17 2020
May 17 2020
nipkow committed rISABELLE57ace76cbffa: another AVL tree version.
another AVL tree version
adapt to Isabelle 07c85c68ff03