isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle