src/HOL/Hoare/hoare_syntax.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-02-21 wenzelm 2014-02-21 reduced ML warnings;
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2013-04-10 wenzelm 2013-04-10 more antiquotations;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-03-29 wenzelm 2011-03-29 use shared copy of hoare_syntax.ML; misc tuning;