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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
20170803, by blanchet
updated CVC4 component to official 1.5 release
20170803, by blanchet
merged
20170803, by paulson
eliminated more "guess", etc.
20170803, by paulson
merged
20170803, by paulson
more tidying
20170803, by paulson
more tidying up
20170803, by paulson
merged
20170803, by paulson
merged
20170803, by paulson
removed all "guess"
20170802, by paulson
tuned
20170803, by nipkow
merged
20170803, by nipkow
added lemmas
20170803, by nipkow
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
20170802, by haftmann
merged
20170803, by nipkow
generalized lemma
20170802, by nipkow
tuned references
20170801, by haftmann
fixed another horrible proof
20170802, by paulson
misc tuning and modernization;
20170801, by wenzelm
isabelle update_cartouches c t;
20170801, by wenzelm
misc tuning and modernization;
20170801, by wenzelm
new lemma
20170801, by nipkow
more explicit Argo proof traces; more correct proof replay for term applications
20170801, by boehmes
more cleanup of Tagged_Division
20170731, by paulson
partial cleanup of the horrible Tagged_Division
20170730, by paulson
introduced option for natasint in SMT
20170728, by blanchet
polytopes: simplical subdivisions, etc.
20170727, by paulson
New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
20170726, by paulson
moved transitive_stepwise_le into Nat, where it belongs
20170726, by paulson
refactored some HORRIBLE integration proofs
20170724, by paulson
merged
20170720, by Lars Hupel
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
20170720, by Lars Hupel
tuned code setup
20170720, by Lars Hupel
strengthened tactic
20170720, by blanchet
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
20170720, by paulson
strengthened tactic (for 'fun' BNF)
20170719, by blanchet
new material: Colinearity, convex sets, polytopes
20170719, by paulson
poles and residues of the Gamma function
20170718, by eberlm
merged
20170718, by Andreas Lochbihler
new derived targets for evaluating Haskell and Scala programs
20170717, by Andreas Lochbihler
Printing natural numbers as numerals in evaluation
20170717, by eberlm
fmap is finite
20170716, by Lars Hupel
facts about cardinality of vector type
20170715, by eberlm
Adapted Approximation_Bounds to changes in Multiset
20170715, by eberlm
Simprocs for roots of numerals
20170715, by eberlm
Updated NEWS
20170715, by eberlm
HOLAnalysis: Infinite products
20170715, by eberlm
More material on powers for HOLComputational_Algebra/HOLNumber_Theory
20170715, by eberlm
additional lemmas for State_Monad, courtesy of Andreas Lochbihler
20170712, by Lars Hupel
more material on finite maps
20170712, by Lars Hupel
redundant since c6714a9562ae
20170712, by traytel
store the unfolded definitions of the lifted bnf constants under "_def" name
20170711, by traytel
state monad
20170711, by Lars Hupel
State_Monad ~> Open_State_Syntax
20170711, by Lars Hupel
more material on fmaps
20170711, by Lars Hupel
canonical representation for fmaps is fmlookup
20170711, by Lars Hupel
fmaps are countable
20170711, by Lars Hupel
merged
20170711, by Lars Hupel
card_0_eq ~> fcard_0_eq
20170711, by Lars Hupel
material from $AFP/Formula_Derivatives/FSet_More
20170711, by Lars Hupel
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
tip