explicit Simplifier.global_context;

recovered header;

eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;

inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;

use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);

added Specification.axiom convenience;

detect OFCLASS() axioms in Nitpick; this is necessary now that "Thy.all_axioms_of" returns such axiom (starting with change 46cfc4b8112e)

merged

contextifying the compilation of the predicate compiler

removed unused Predicate_Compile_Set

avoiding fishing for split_asm rule in the predicate compiler

contextifying the proof procedure in the predicate compiler

making flat triples to nested tuple to remove general triple functions

reduced the debug output functions from 2 to 1

some improvements thanks to Makarius source code review

adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises

enabling a previously broken example of the predicate compiler again

improving handling of case expressions in predicate rewriting

adding depth_limited_random compilation to predicate compiler

a new simpler random compilation for the predicate compiler

reviving the classical depth-limited computation in the predicate compiler

cleaning the function flattening

generalized split transformation in the function flattening

only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code

restructuring function flattening

renaming mk_prems to flatten in the function flattening

simplifying function flattening

removed warning_count (known causes for warnings have been resolved)

remove the iteration counter from Sledgehammer's minimizer

merged