2013-06-15 haftmann 2013-06-15 documentation on code_printing and code_identifier
2013-06-15 haftmann 2013-06-15 more consistent parsing and reading of classes and type constructors
2013-06-14 kleing 2013-06-14 another example lemma
2013-06-13 blanchet 2013-06-13 store more theorems in data structure
2013-06-13 blanchet 2013-06-13 tuning
2013-06-13 nipkow 2013-06-13 simplified proofs
2013-06-12 kleing 2013-06-12 prefer xsymbol for book
2013-06-12 nipkow 2013-06-12 same order of properties as in While rule
2013-06-11 kleing 2013-06-11 some comments on syntax and automation setup
2013-06-11 smolkas 2013-06-11 uncheck terms before annotation to avoid awkward syntax
2013-06-11 blanchet 2013-06-11 tuning
2013-06-11 blanchet 2013-06-11 tuning
2013-06-11 smolkas 2013-06-11 make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
2013-06-11 haftmann 2013-06-11 reflexive nbe equation for equality on String.literal
2013-06-10 haftmann 2013-06-10 tuned whitespace
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