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