more idiomatic handling of latex typewriter type setting

more canonical type setting of type writer code examples

resynchronize isabelle.sty

reverted cs 5aced2f43837 -- no need for hardwired latex command here

reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter

reverted cs 07549694e2f1

shifted abstraction over imperative print mode

removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned

moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule

exporting the generic version instead of the context version in quickcheck

splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests

adding a mutual recursive example for named alternative rules for the predicate compiler

handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types

improving naming of assumptions in code_pred

adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim

handling equivalences smarter in the predicate compiler

removing duplicate rewrite rule from simpset in predicate compiler

rewriting function mk_Eval_of in predicate compiler

merged

improved and tuned external codegen tool

make SML/NJ happy

CONTRIBUTORS and NEWS

corrections and tuning

merged

merged

merged

tuned

persistent session-panel.selection;

slightly more robust EditBus plumbing wrt. Document_View/Document_Model;

permissive exit;