src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
2013-10-01 blanchet 2013-10-01 renamed theory file
2013-09-26 blanchet 2013-09-26 made tactic more robust in case somebody specified a discriminator for a one-constructor type
2013-09-26 blanchet 2013-09-26 generate "sel_splits(_asm)" theorems
2013-09-26 blanchet 2013-09-26 generate "sel_exhaust" theorem
2013-09-24 blanchet 2013-09-24 renamed generated property
2013-09-18 blanchet 2013-09-18 tuned tactics
2013-08-12 blanchet 2013-08-12 define case constant from other 'free constructor' axioms
2013-08-12 blanchet 2013-08-12 introduced case tactics
2013-08-12 blanchet 2013-08-12 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-05-12 wenzelm 2013-05-12 proper context;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-27 blanchet 2013-04-27 tuned ML and thy file names