src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
Sat, 21 Dec 2013 09:44:28 +0100 blanchet renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
Thu, 19 Dec 2013 21:49:30 +0100 blanchet implemented 'exhaustive' option in tactic
Sun, 01 Dec 2013 19:32:57 +0100 panny more work towards "exhaustive"
Wed, 06 Nov 2013 13:00:45 +0100 blanchet removed dead code
Mon, 04 Nov 2013 16:53:43 +0100 blanchet split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
less more (0) tip