2013-06-10 haftmann 2013-06-10 dropped relics of ancient binary numeral case study
2013-06-10 nipkow 2013-06-10 merged
2013-06-10 nipkow 2013-06-10 all headings in upper case
2013-06-10 huffman 2013-06-10 more int/nat transfer rules; examples of new untransferred attribute
2013-06-10 huffman 2013-06-10 more transfer rules for sets
2013-06-10 huffman 2013-06-10 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
2013-06-10 blanchet 2013-06-10 use right context when exporting variables (cf. AFP Coinductive_List failures)
2013-06-10 blanchet 2013-06-10 keep track of nested BNFs
2013-06-10 blanchet 2013-06-10 tuning
2013-06-08 huffman 2013-06-08 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
2013-06-07 blanchet 2013-06-07 SPASS has more Uppercase keywords than I was fearing -- better always append _
2013-06-07 blanchet 2013-06-07 merge
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 adapted example (cf. 78a3d5006cf1)
2013-06-07 blanchet 2013-06-07 code simplifications (cf. 78a3d5006cf1)
2013-06-07 blanchet 2013-06-07 killed dead code
2013-06-07 blanchet 2013-06-07 changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
2013-06-07 blanchet 2013-06-07 killed dead code
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 nipkow 2013-06-07 tuned
2013-06-07 nipkow 2013-06-07 tuned variable names
2013-06-07 nipkow 2013-06-07 tuned
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 [mq]: tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 fixed failure in coinduction rule tactic
2013-06-06 blanchet 2013-06-06 too much qualification is like too little
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 merge
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 nipkow 2013-06-06 tuned defs
2013-06-06 blanchet 2013-06-06 avoid duplicate call to "mk_fold_rec_args_types" function
2013-06-06 blanchet 2013-06-06 continuation of f461dca57c66
2013-06-06 blanchet 2013-06-06 renamed ML variables
2013-06-06 blanchet 2013-06-06 tuned record field names to avoid confusion between low-level and high-level constants/theorems
2013-06-06 blanchet 2013-06-06 tuned signature
2013-06-06 blanchet 2013-06-06 support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
2013-06-06 blanchet 2013-06-06 tuned ML variable names
2013-06-05 kuncar 2013-06-05 transfer rule for listsum
2013-06-05 kuncar 2013-06-05 more reflexivity rules (for OO)
2013-06-05 blanchet 2013-06-05 tuning
2013-06-05 blanchet 2013-06-05 avoid code duplication
2013-06-05 blanchet 2013-06-05 eliminated dead argument