preplay subblocks

renamed sledgehammer_shrink to sledgehammer_compress

dont skolemize conjecture

introduced subblock in isar_step datatype for conjecture herbrandization

write_pdf for JFreeChart;

reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck

merged

instantiate finite_UNIV and card_UNIV for finfun type

merged

more parallel proofs in 'nominal_datatype', although sequential dark matter remains;

tuned proof;

obsolete;

tuned proofs;

tuned signature -- legacy packages might want to fork proofs as well;

merged

implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug

consolidation of library theories on product orders

type lifting setup for code numeral types

factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions

abandoned theory Plain

tuned;

clarified default according to etc/options;

Java assumes regular "re-parenting" window manager;

merged