introduce a proper view on checkInsert
[~helmut/bidiragda.git] / CheckInsert.agda
2013-01-12 Helmut Grohneintroduce a proper view on checkInsert
2013-01-10 Helmut GrohneMerge branch 'newlemma'
2013-01-10 Helmut Grohnereduce a precondition of lemma-checkInsert-lookupM
2013-01-09 Helmut Grohneadd new lemma-checkInsert-lookupM
2013-01-09 Helmut Grohnesimplify lemma-lookupM-checkInsert using case-split
2012-11-22 Helmut Grohneshorten line length of lemma-lookupM-checkInsert
2012-11-02 Helmut Grohnerewrite checkInsert using "... |" notation
2012-10-25 Helmut Grohnerename lemma-from-just to just-injective
2012-10-22 Helmut GrohneMerge branch 'modparam'
2012-10-22 Helmut Grohnefinally parameterize CheckInsert
2012-09-26 Helmut Grohneuse _\==n_ and _\notin_ instead of \neg
2012-09-26 Helmut Grohneimport [_] instead of Reveal_is_
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-18 Helmut Grohneone more application of lemma-just\==nnothing
2012-06-05 Helmut Grohnemove checkInsert and related properties to CheckInsert...