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.
basic setup for chapter "The Isabelle/Isar Framework";
20090209, by wenzelm
more refs;
20090209, by wenzelm
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
20090202, by wenzelm
export lexicographic_order_tac
20090202, by krauss
fix potential incompleteness in SAT encoding
20090202, by krauss
avoid name clash of generated modules and includes
20090202, by haftmann
strict check for locale target
20090202, by haftmann
fixed proposition slip
20090202, by haftmann
added Mapping.thy to Library
20090202, by haftmann
dropped Id
20090202, by haftmann
updated type class section
20090202, by haftmann
updated class documentation
20090202, by haftmann
merged
20090201, by haftmann
added State_Monad theory in session
20090201, by haftmann
proper declared constants in class expressions
20090201, by haftmann
merged
20090131, by nipkow
added some simp rules
20090131, by nipkow
fixed case
20090130, by krauss
Fixed theory name
20090130, by chaieb
Added Formal_Power_Series_Examples to HOLex image
20090130, by chaieb
Some applications of formal power Series
20090130, by chaieb
Added real related theorems from Fact.thy
20090130, by chaieb
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
20090130, by chaieb
moved upwards in thy graph, real related theorems moved to Transcendental.thy
20090130, by chaieb
Enclosed name containing _'s in @{text ...} antiquotation to make document
20090129, by berghofe
Added strong congruence rule for UN.
20090129, by berghofe
Added abs_def attribute.
20090129, by berghofe
removed definition of funpow , reusing that of Relation_Power
20090129, by chaieb
Added Formal_Power_Series in imports
20090129, by chaieb
A formalization of formal power series
20090129, by chaieb
Inserted Formal_Power_Series.thy under Library
20090129, by chaieb
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20090129, by paulson
Minor reorganisation of the Skolemization code
20090129, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20090113, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20090109, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20081219, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20081215, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20081211, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20081210, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20081210, by paulson
Updated comments.
20081205, by paulson
dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
20090129, by chaieb
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
20090128, by chaieb
merged
20090129, by nipkow
commented out unused lemmas. May need to be put back by Brian.
20090129, by nipkow

20090128, by nipkow
removed spurious conflic msg
20090128, by nipkow
merged
20090128, by nipkow
merged  resolving conflics
20090128, by nipkow
Replaced group_ and ring_simps by algebra_simps;
20090128, by nipkow
merged
20090128, by haftmann
explicit check for exactly one type variable in class specification elements
20090128, by haftmann
merged
20090128, by huffman
merged
20090127, by huffman
removed use of prev_cont_thms reference
20090122, by huffman
merged
20090122, by huffman
add lemmas about div/mod with multiplication
20090121, by huffman
add lemmas about smult
20090121, by huffman
merged
20090128, by haftmann
slightly adapted towards more uniformity with div/mod on nat
20090128, by haftmann
less
more

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