src/HOL/Tools/BNF/bnf_def.ML
Thu, 10 Apr 2014 17:48:16 +0200 kuncar don't forget to init Interpretation and transfer theorems in the interpretation hook
Thu, 03 Apr 2014 10:51:24 +0200 blanchet added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
Tue, 01 Apr 2014 10:51:29 +0200 blanchet added BNF interpretation hook
Mon, 10 Mar 2014 13:23:16 +0100 traytel unfold intermediate definitions after sealing the bnf
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Mon, 03 Mar 2014 12:48:20 +0100 blanchet make 'typedef' optional, depending on size of original type
Fri, 14 Feb 2014 15:03:24 +0100 blanchet allow different functions to recurse on the same type, like in the old package
Wed, 12 Feb 2014 17:36:00 +0100 blanchet iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
Wed, 12 Feb 2014 08:35:56 +0100 blanchet more liberal merging of BNFs and constructor sugar
Fri, 07 Feb 2014 10:44:04 +0100 blanchet reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
Thu, 06 Feb 2014 17:05:47 +0100 blanchet allow multiple registration of the same type, the last wins
Fri, 31 Jan 2014 10:02:36 +0100 traytel less hermetic tactics
Mon, 20 Jan 2014 18:24:56 +0100 blanchet adjusted comments
Mon, 20 Jan 2014 18:24:56 +0100 blanchet avoid nested 'Tools' directories
less more (0) tip