Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
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.
Use conversions instead of simplifier. tuned
20080305, by krauss
added new example
20080304, by urbanc
tuned
20080303, by haftmann
continued localization
20080303, by haftmann
new theory of redblack trees, an efficient implementation of finite maps.
20080303, by krauss
Generalized Zorn and added wellordering theorem
20080302, by nipkow
tuned ML code, more antiquotations;
20080301, by wenzelm
misc cleanup of embedded ML code;
20080301, by wenzelm
added @{const} antiquotation;
20080301, by wenzelm
use more antiquotations;
20080301, by wenzelm
unused_thms: print via official context (ProofContext.pretty_fact),
20080228, by wenzelm
Added function for finding unused theorems.
20080228, by berghofe
Added unused_thms command.
20080228, by berghofe
import all 'special code' types
20080228, by haftmann
added code generator setup
20080228, by haftmann
Transitive_Closure: induct and cases rules now declare proper case_names;
20080228, by wenzelm
Transitive_Closure: induct and cases rules now declare proper case_names;
20080228, by wenzelm
rtranclp_induct, tranclp_induct: added case_names;
20080228, by wenzelm
tuned
20080228, by nipkow
removed legacy ML bindings;
20080228, by wenzelm
tuned syntax declaration;
20080228, by wenzelm
wf_trancl: structured proof;
20080228, by wenzelm
rtranclE, tranclE: tuned statement, added case_names;
20080228, by wenzelm
renamed ListSpace to ListVector;
20080228, by wenzelm
added HOLLibrary;
20080228, by wenzelm
more precise handling of "group" for termination;
20080227, by wenzelm
added theories for imperative HOL
20080227, by haftmann
added theory for countable types
20080227, by haftmann
added theory for reflected types
20080227, by haftmann
proper merge of base sorts
20080227, by haftmann
Renamed ListSpace to ListVector
20080227, by nipkow
Fixed dependency on Dense_Linear_Order
20080227, by chaieb
removed some debugging output from trace
20080227, by schirmer
Loads Dense_Linear_Order (needed dlo_simps)
20080227, by chaieb
Fixed dependencies for proofs  ferrack needed
20080227, by chaieb
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
20080227, by chaieb
fixed dependencies
20080227, by chaieb
Removed theorems from default simpset
20080227, by chaieb
Fixed proofs
20080227, by chaieb
Loads Dense_Linear_Order.thy
20080227, by chaieb
loads Tools/Qelim/qelim.ML
20080227, by chaieb
HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
20080227, by chaieb
Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy
20080227, by chaieb
other UNIV lemmas
20080226, by haftmann
some more primrec
20080226, by haftmann
class itself works around a problem with class interpretation in class finite
20080226, by haftmann
moved some set lemmas from Set.thy here
20080226, by haftmann
tuned heading
20080226, by haftmann
char and nibble are finite
20080226, by haftmann
moved some set lemmas to Set.thy
20080226, by haftmann
tuned proofs
20080226, by haftmann
tuned document;
20080226, by wenzelm
tuned document;
20080226, by wenzelm
Added useful general lemmas from the work with the HeapMonad
20080226, by bulwahn
some steps towards automated generators
20080226, by haftmann
operation collapse
20080226, by haftmann
Zero/Suc recursion combinator for type index
20080226, by haftmann
added accidental omissions
20080226, by haftmann
thm_deps: sort result;
20080225, by wenzelm
tuned msg;
20080225, by wenzelm
less
more

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