Summary
- some updates and clarification on Assumption.export_term;
- new theorem has_integral_UN
- updated to jdk-17.0.2+8;
- used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
- NEWS
- added Mirabelle option "-y" for dry run
- tuned garbage optimization
- added cpu time (in ms) to Mirabelle run_action output
- added Mirabelle option -r to randomize the goals before selection
- A new lemma about inverse image
- proper treatment of $let variables in symbol table in Sledgehammer
- removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer
Summary
- Removal of a lemma (now in the libraries) and a few tweaks
The file was modified | thys/Szemeredi_Regularity/Szemeredi.thy |