Thu, 10 Apr 2014 18:13:44 +0200removed obsolete doc_dump option (see also 892061142ba6);
wenzelm [Thu, 10 Apr 2014 18:13:44 +0200] rev 57872
removed obsolete doc_dump option (see also 892061142ba6);

Wed, 09 Apr 2014 14:08:25 +0200restoring notion of primitive vs. derived operations in terms of generated code;
haftmann [Wed, 09 Apr 2014 14:08:25 +0200] rev 57871
restoring notion of primitive vs. derived operations in terms of generated code;
established _paramatric suffix for parametricity rules

Wed, 09 Apr 2014 14:08:18 +0200removed duplication and tuned
haftmann [Wed, 09 Apr 2014 14:08:18 +0200] rev 57870
removed duplication and tuned

Thu, 10 Apr 2014 17:48:54 +0200make list_all an abbreviation of pred_list - prevent duplication
kuncar [Thu, 10 Apr 2014 17:48:54 +0200] rev 57869
make list_all an abbreviation of pred_list - prevent duplication

Thu, 10 Apr 2014 17:48:33 +0200add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons
kuncar [Thu, 10 Apr 2014 17:48:33 +0200] rev 57868
add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons

Thu, 10 Apr 2014 17:48:32 +0200simplify and fix theories thanks to 356a5efdb278
kuncar [Thu, 10 Apr 2014 17:48:32 +0200] rev 57867
simplify and fix theories thanks to 356a5efdb278

Thu, 10 Apr 2014 17:48:18 +0200setup for Transfer and Lifting from BNF; tuned thm names
kuncar [Thu, 10 Apr 2014 17:48:18 +0200] rev 57866
setup for Transfer and Lifting from BNF; tuned thm names

Thu, 10 Apr 2014 17:48:17 +0200revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
kuncar [Thu, 10 Apr 2014 17:48:17 +0200] rev 57865
revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created

Thu, 10 Apr 2014 17:48:16 +0200don't forget to init Interpretation and transfer theorems in the interpretation hook
kuncar [Thu, 10 Apr 2014 17:48:16 +0200] rev 57864
don't forget to init Interpretation and transfer theorems in the interpretation hook

Thu, 10 Apr 2014 17:48:16 +0200export theorems
kuncar [Thu, 10 Apr 2014 17:48:16 +0200] rev 57863
export theorems