2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
2013-11-05 blanchet 2013-11-05 added some N2M caching
2013-11-05 blanchet 2013-11-05 also generalize fixed types
2013-11-05 blanchet 2013-11-05 generalize types when synthetizing n2m (co)recursors, to facilitate reuse
2013-11-05 blanchet 2013-11-05 nicer error message in case of duplicates
2013-11-05 kleing 2013-11-05 use int example like in the rest of IMP (instead of nat)
2013-11-04 haftmann 2013-11-04 dropped dead code
2013-11-04 haftmann 2013-11-04 fact generalization and name consolidation
2013-11-04 haftmann 2013-11-04 streamlined setup of linear arithmetic
2013-11-04 blanchet 2013-11-04 make 'try0' return faster when invoked as part of 'try'
2013-11-04 blanchet 2013-11-04 careful with lists of different lengths
2013-11-04 blanchet 2013-11-04 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
2013-11-04 blanchet 2013-11-04 better error handling
2013-11-04 traytel 2013-11-04 more robust treatment of dead variables in n2m
2013-11-04 blanchet 2013-11-04 more robust n2m w.r.t. 'let's
2013-11-04 blanchet 2013-11-04 tuning
2013-11-04 blanchet 2013-11-04 strengthened tactic
2013-11-04 blanchet 2013-11-04 made n2m code more robust w.r.t. advanced constructs (e.g. lambdas)
2013-11-04 blanchet 2013-11-04 handle constructor syntax in n2m primcorec
2013-11-04 blanchet 2013-11-04 typo
2013-11-04 blanchet 2013-11-04 made sugared 'coinduct' theorem construction n2m-proof
2013-11-04 blanchet 2013-11-04 moved code around
2013-11-04 blanchet 2013-11-04 tuning
2013-11-04 blanchet 2013-11-04 make code more robust w.r.t. applied/unapplied map (primrec vs. primcorec)
2013-11-04 blanchet 2013-11-04 conceal definition
2013-11-02 nipkow 2013-11-02 more exercises
2013-11-02 nipkow 2013-11-02 more exercises
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-31 blanchet 2013-10-31 generate stable names for axioms
2013-10-31 haftmann 2013-10-31 purely algebraic foundation for even/odd
2013-10-31 haftmann 2013-10-31 moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas; tuned presburger
2013-10-31 haftmann 2013-10-31 explicit type class for modelling even/odd parity
2013-10-31 haftmann 2013-10-31 generalized of_bool conversion
2013-10-31 haftmann 2013-10-31 separated bit operations on type bit from generic syntactic bit operations
2013-10-31 haftmann 2013-10-31 restructed
2013-10-31 haftmann 2013-10-31 generalised lemma
2013-10-31 haftmann 2013-10-31 more lemmas on division
2013-10-31 haftmann 2013-10-31 more convenient place for a theory in solitariness
2013-10-31 haftmann 2013-10-31 consolidated clone theory
2013-10-31 nipkow 2013-10-31 more exercises
2013-10-30 nipkow 2013-10-30 tuned text
2013-10-29 berghofe 2013-10-29 inst_lift now fully instantiates context to avoid problems with loose bound variables
2013-10-29 panny 2013-10-29 include corecursive functions' arguments in callssss
2013-10-29 nipkow 2013-10-29 more exercises
2013-10-28 nipkow 2013-10-28 merged
2013-10-28 nipkow 2013-10-28 more exercises
2013-10-27 blanchet 2013-10-27 commented out vaporware
2013-10-26 nipkow 2013-10-26 more exercises
2013-10-26 blanchet 2013-10-26 tuning
2013-10-26 blanchet 2013-10-26 tuning
2013-10-26 blanchet 2013-10-26 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
2013-10-26 blanchet 2013-10-26 align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
2013-10-26 blanchet 2013-10-26 convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
2013-10-26 blanchet 2013-10-26 tuned error message
2013-10-25 nipkow 2013-10-25 more exercises
2013-10-24 blanchet 2013-10-24 handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
2013-10-24 blanchet 2013-10-24 tuning
2013-10-24 blanchet 2013-10-24 more correct (!) types for recursive calls
2013-10-24 blanchet 2013-10-24 watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
2013-10-24 blanchet 2013-10-24 got rid of annoying duplicate rewrite rule warnings