tuned signature;

clarified modules;

clarified modules;

unused;

tuned signature;

clarified signature: replaced Sessions.Deps by Sessions.Structure from HTML_Context;

tuned;

clarified signature: avoid constants from Sessions.Structure within Session.Base;

clarified signature: avoid object-oriented HTML_Context; clarified theory_qualifier --- belongs to the overall Sessions.Structure;

tuned type signature

tuned type signature

streamlined theorems

more thorough split rules for div and mod on numerals, tuned split rules setup

streamlined simpset building, avoiding duplicated rewrite rules

consolidated attribute name

streamlined theorems

streamlined theorems and sections

streamlined primitive definitions for integer division

reintroduced SPASS to the mix

tweaked generation of Isar proofs

tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s

tuned comments;

updated to sumatra_pdf-3.4.6;

proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;

revived 'try0' and 'smart' Isar proofs in Sledgehammer

Cleanup of NonstandardAnalysis

A bit of cleaning up

The same, without adding a new simprule

moved some material from Sum_of_Powers

merged

clarified signature;

clarified theory_names with exported content;