tuned signature;

more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;

more conventional tactic setup;

eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);

prefer high-level elim_format;

discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;

method setup;

simplified use of tacticals;

comment;

tuned signature, according to actual usage of these operations;

tuned signature;

normalized aliases;

elininated unused INTLEAVE;

eliminated unused rewrite_goal_rule;

eliminated unused subgoals_tac;

eliminated obsolete aliases;

eliminated obsolete aliases;

tuned;

merged, resolving trivial conflicts;

merged;

new SPASS options

making num_mutations a configuration that can be changed with the mutabelle bash command

making max_mutants an option that can be changed in the Mutabelle-script

increase timeout to 30 seconds; changing mutabelle script

parse clauses generated from several formulas

be more gentle when generating KBO weights

update SPASS slices

more specification of the quotient package in IsarRef

specification of the quotient package

tune KBO weight code

minor DFG fix

new SPASS slices

improved KBO weights -- beware of explicit applications

added possibility of generating KBO weights to DFG problems

Generalize the compositional preservation theorems

use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")

removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly

beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms

fixed arity error

tuning

renamed type encoding

adding some forbidden constant names for mutabelle

mutabelle ignores theorems with internal constants

tuned

merged

simplified code generation

remove option that's on by default

no need for a script/mega-hack with the new SPASS

cleaned up new SPASS parsing

tuning

merged

adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists

tuning to remove ML warnings

removed double filtering of type args

adding a quickcheck example about functions and sets

removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)

adding a remark about lemma which is too special and should be removed

another try to improve code generation of set equality (cf. da32cf32c0c7)

beautifying definitions of check_all and adding instance for finite_4

Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.