src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
Fri, 10 Jan 2014 14:39:37 +0100 blanchet fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
Fri, 10 Jan 2014 14:39:37 +0100 blanchet only destruct cases equipped with the right stuff (in particular, 'sel_split')
Fri, 10 Jan 2014 14:39:37 +0100 blanchet generate 'disc_iff' for all discriminators
Fri, 10 Jan 2014 14:39:37 +0100 blanchet use 'disc_iff' as simp rules whenever possible + clean up '= True', '= False', etc.
Fri, 10 Jan 2014 14:39:37 +0100 blanchet exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial
Fri, 10 Jan 2014 09:48:11 +0100 blanchet fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
Thu, 09 Jan 2014 19:10:35 +0100 panny do not use wrong constructor in auto-generated proof goal
Thu, 09 Jan 2014 17:13:05 +0100 blanchet tuned error message
Thu, 09 Jan 2014 16:40:50 +0100 blanchet reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
Thu, 09 Jan 2014 15:49:19 +0100 blanchet strengthened tactics w.r.t. 'lets' and tuples
Thu, 09 Jan 2014 15:07:25 +0100 blanchet for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
Wed, 08 Jan 2014 17:26:42 +0100 panny match order of generated theorems to user input;
Fri, 03 Jan 2014 14:38:13 +0100 blanchet proper name generation to avoid clash with 'P' in user specification
Fri, 03 Jan 2014 14:14:16 +0100 blanchet more SML-ish (less Haskell-ish) naming convention
Fri, 03 Jan 2014 14:04:37 +0100 blanchet strengthened tactic
Fri, 03 Jan 2014 13:55:34 +0100 blanchet refactoring
Fri, 03 Jan 2014 11:26:44 +0100 blanchet instantiate schematics as projections to avoid HOU trouble
Thu, 02 Jan 2014 23:44:31 +0100 blanchet avoid schematic variable in goal, which sometimes gets instantiated by tactic
Thu, 02 Jan 2014 20:51:09 +0100 blanchet made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
Thu, 02 Jan 2014 09:50:22 +0100 blanchet consider code as exhaustive
Thu, 02 Jan 2014 09:50:22 +0100 blanchet proper handling of corner case, take 2
Thu, 02 Jan 2014 09:50:22 +0100 blanchet robustness
Thu, 02 Jan 2014 09:50:22 +0100 blanchet properly synchronize parallel lists
Thu, 02 Jan 2014 09:50:22 +0100 blanchet graceful handling of one-constructor case
Thu, 02 Jan 2014 09:50:22 +0100 blanchet made tactic handle gracefully the case of missing constructors
Thu, 02 Jan 2014 09:50:22 +0100 blanchet removed 'nchotomy' property
Thu, 02 Jan 2014 09:50:22 +0100 blanchet don't generate any proof obligation for implicit (de facto) exclusiveness
Thu, 02 Jan 2014 09:50:22 +0100 blanchet detect syntactic exhaustiveness
Thu, 02 Jan 2014 09:50:22 +0100 blanchet internally allow different values for 'exhaustive' for different constructors
Thu, 02 Jan 2014 09:50:22 +0100 blanchet internally allow different values for 'sequential' for different constructors
Thu, 02 Jan 2014 09:50:22 +0100 blanchet use same name for feature internally as in user interface, to facilitate grepping
Thu, 02 Jan 2014 09:50:22 +0100 blanchet generate 'disc_iff' property in 'primcorec'
Thu, 02 Jan 2014 09:50:22 +0100 blanchet added tactic to prove 'disc_iff' properties in 'primcorec'
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Sat, 21 Dec 2013 09:44:30 +0100 blanchet generate exhaust from nchotomy
Sat, 21 Dec 2013 09:44:28 +0100 blanchet renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
Fri, 20 Dec 2013 11:34:07 +0100 blanchet note manually proved exclusiveness property
Fri, 20 Dec 2013 11:12:51 +0100 blanchet note exhaust proof obligation
Thu, 19 Dec 2013 21:49:30 +0100 blanchet implemented 'exhaustive' option in tactic
Wed, 18 Dec 2013 14:50:25 +0100 panny pass down user input in more cases in order to preserve "let"s etc.
Wed, 18 Dec 2013 14:06:34 +0100 panny pass auto-proved exhaustiveness properties to tactic;
Mon, 02 Dec 2013 19:49:34 +0100 panny generate "code" theorems for incomplete definitions
Sun, 01 Dec 2013 19:32:57 +0100 panny more work towards "exhaustive"
Mon, 25 Nov 2013 20:25:22 +0100 panny prevent exception when equations for a function are missing;
Wed, 06 Nov 2013 13:00:45 +0100 blanchet removed dead code
Wed, 06 Nov 2013 12:47:50 +0100 blanchet take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case
Tue, 05 Nov 2013 16:53:40 +0100 blanchet avoid subtle failure in the presence of top sort
Tue, 05 Nov 2013 16:47:10 +0100 blanchet tuning
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