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 tip

added missing preprocessing step for extraction (due to Stefan Berghofer)
2020-05-15, by Manuel Eberl
new HOL simproc: eliminate_false_implies
2020-05-13, by Manuel Eberl
added lemma
2020-05-14, by nipkow
Tuned some proofs in HOL-Analysis
2020-05-14, by Manuel Eberl
The Uniq quantifier for FOL too
2020-05-14, by paulson
generalised pigeonhole principle in HOL-Library.FuncSet
2020-05-13, by Manuel Eberl
new constant power_int in HOL
2020-05-13, by Manuel Eberl
New HOL simproc 'datatype_no_proper_subterm'
2020-05-04, by Manuel Eberl
merged
2020-05-12, by paulson
Fixes for Sup{} = (0::nat)
2020-05-12, by paulson
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
2020-05-12, by paulson
clarified session imports: avoid bulky HOL-Library image;
2020-05-12, by wenzelm
tuned -- avoid warning;
2020-05-12, by wenzelm
"app" -> "join" for RBTs
2020-05-12, by nipkow
"app" -> "join" for uniformity with Join theory; tuned defs
2020-05-12, by nipkow
added top-level functions and tuned
2020-05-11, by nipkow
the Uniq quantifier
2020-05-11, by paulson
modernized notation for bit operations
2020-05-09, by haftmann
merged
2020-05-08, by nipkow
avoid hidden undef cases
2020-05-08, by nipkow
explicit mask operation for bits
2020-05-08, by haftmann
prefer _ mod 2 over of_bool (odd _)
2020-05-08, by haftmann
less aggressive default simp rules
2020-05-08, by haftmann
simplified and tuned
2020-05-06, by nipkow
tuned
2020-05-06, by nipkow
tuned
2020-05-06, by nipkow
tuned proofs
2020-05-05, by nipkow
tuned var. names
2020-05-05, by nipkow
tuned var. names
2020-05-04, by nipkow
AVL trees with balance tags
2020-05-04, by nipkow
A little more tidying up
2020-04-29, by paulson
tuned
2020-04-29, by nipkow
merged
2020-04-28, by nipkow
tuned
2020-04-28, by nipkow
merged
2020-04-28, by wenzelm
added "isabelle sessions" tool;
2020-04-28, by wenzelm
tuned messages;
2020-04-28, by wenzelm
use abs(h l - h r) instead of 3 cases, tuned proofs
2020-04-28, by nipkow
added lemmas
2020-04-27, by nipkow
simplified construction of binary bit operations
2020-04-27, by haftmann
temporarily revert change which does not work as expected
2020-04-25, by haftmann
more rules
2020-04-25, by haftmann
added Height_Balanced_Trees
2020-04-25, by nipkow
documentation of relevant ideas
2020-04-24, by haftmann
numeral rules for take_bit / drop_bit on int
2020-04-24, by haftmann
opaque export does not work as expected in presence of dependent instances
2020-04-24, by haftmann
merged
2020-04-23, by nipkow
tuned document
2020-04-23, by nipkow
split AVL_Set.thy
2020-04-23, by nipkow
avoid passing chained facts twice to preplay in Sledgehammer
2020-04-23, by blanchet
tweaked Vampire's options + tuning
2020-04-23, by blanchet
more robust Isabelle_System.init (amending c0bc99aad936): avoid non-termination on Windows (java.lang.StackOverflowError);
2020-04-23, by wenzelm
back to more modest (but uniform) Java stack, see 97fc4f657bda;
2020-04-23, by wenzelm
more generous Java memory, also hoping to prevent spurious java.lang.StackOverflowError in isabelle_cronjob;
2020-04-23, by wenzelm
added lemmas
2020-04-23, by nipkow
hooks for foundational terms: protection of foundational terms during simplification
2020-04-21, by haftmann
merged
2020-04-22, by wenzelm
merged
2020-04-22, by wenzelm
avoid deprecated operations;
2020-04-22, by wenzelm
tuned -- avoid odd compiler warning;
2020-04-22, by wenzelm

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

isabelle