7 weeks ago nipkow 2020-05-22 added simp lemma
7 weeks ago haftmann 2020-05-21 slightly more specific implementations
7 weeks ago haftmann 2020-05-21 tuned module name space for generated code
7 weeks ago nipkow 2020-05-21 unused alias
7 weeks ago haftmann 2020-05-20 generalized and augmented
7 weeks ago wenzelm 2020-05-20 clarified signature;
7 weeks ago wenzelm 2020-05-20 clarified modules;
7 weeks ago paulson 2020-05-20 A few new theorems, plus some tidying up
7 weeks ago haftmann 2020-05-20 corrected spelling and tuned whitespace
7 weeks ago nipkow 2020-05-19 tuned
8 weeks ago wenzelm 2020-05-18 follow Phabricator update 2020 Week 19;
8 weeks ago nipkow 2020-05-17 another AVL tree version
8 weeks ago Manuel Eberl 2020-05-15 added missing preprocessing step for extraction (due to Stefan Berghofer)
2 months ago Manuel Eberl 2020-05-13 new HOL simproc: eliminate_false_implies
8 weeks ago nipkow 2020-05-14 added lemma
2 months ago Manuel Eberl 2020-05-14 Tuned some proofs in HOL-Analysis
2 months ago paulson 2020-05-14 The Uniq quantifier for FOL too
2 months ago Manuel Eberl 2020-05-13 generalised pigeonhole principle in HOL-Library.FuncSet
2 months ago Manuel Eberl 2020-05-13 new constant power_int in HOL
2 months ago Manuel Eberl 2020-05-04 New HOL simproc 'datatype_no_proper_subterm'
2 months ago paulson 2020-05-12 merged
2 months ago paulson 2020-05-12 Fixes for Sup{} = (0::nat)
2 months ago paulson 2020-05-12 abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
2 months ago wenzelm 2020-05-12 clarified session imports: avoid bulky HOL-Library image;
2 months ago wenzelm 2020-05-12 tuned -- avoid warning;
2 months ago nipkow 2020-05-12 "app" -> "join" for RBTs
2 months ago nipkow 2020-05-12 "app" -> "join" for uniformity with Join theory; tuned defs
2 months ago nipkow 2020-05-11 added top-level functions and tuned
2 months ago paulson 2020-05-11 the Uniq quantifier
2 months ago haftmann 2020-05-09 modernized notation for bit operations
2 months ago nipkow 2020-05-08 merged
2 months ago nipkow 2020-05-08 avoid hidden undef cases
2 months ago haftmann 2020-05-08 explicit mask operation for bits
2 months ago haftmann 2020-05-08 prefer _ mod 2 over of_bool (odd _)
2 months ago haftmann 2020-05-08 less aggressive default simp rules
2 months ago nipkow 2020-05-06 simplified and tuned
2 months ago nipkow 2020-05-06 tuned
2 months ago nipkow 2020-05-06 tuned
2 months ago nipkow 2020-05-05 tuned proofs
2 months ago nipkow 2020-05-05 tuned var. names
2 months ago nipkow 2020-05-04 tuned var. names
2 months ago nipkow 2020-05-04 AVL trees with balance tags
2 months ago paulson 2020-04-29 A little more tidying up
2 months ago nipkow 2020-04-29 tuned
2 months ago nipkow 2020-04-28 merged
2 months ago nipkow 2020-04-28 tuned
2 months ago wenzelm 2020-04-28 merged
2 months ago wenzelm 2020-04-28 added "isabelle sessions" tool;
2 months ago wenzelm 2020-04-28 tuned messages;
2 months ago nipkow 2020-04-28 use abs(h l - h r) instead of 3 cases, tuned proofs
2 months ago nipkow 2020-04-27 added lemmas
2 months ago haftmann 2020-04-27 simplified construction of binary bit operations
2 months ago haftmann 2020-04-25 temporarily revert change which does not work as expected
2 months ago haftmann 2020-04-25 more rules
2 months ago nipkow 2020-04-25 added Height_Balanced_Trees
2 months ago haftmann 2020-04-24 documentation of relevant ideas
2 months ago haftmann 2020-04-24 numeral rules for take_bit / drop_bit on int
2 months ago haftmann 2020-04-24 opaque export does not work as expected in presence of dependent instances
2 months ago nipkow 2020-04-23 merged
2 months ago nipkow 2020-04-23 tuned document