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.
adjusted postprocessort setup
20080703, by haftmann
added lemma antiquotation
20080703, by haftmann
adjusted rep_datatype
20080703, by haftmann
Adapted to changes in perm_simp / swap_simps.
20080703, by berghofe
Replaced all but one occurrence of perm_simp_tac by perm_simproc_app,
20080703, by berghofe
Rewrote code to use swap_simps rather than calc_atm (which tends to
20080703, by berghofe
moved HOLPlain up;
20080702, by wenzelm
rename Doc docsrc;
20080702, by wenzelm
renamed Contents to Dirs to avoid caseconflict with doc/Contents;
20080702, by wenzelm
section > subsection
20080702, by huffman
convert Isabelle CVS to Mercurial;
20080702, by wenzelm
use begin and end for proofs in locales
20080702, by huffman
exclude Distribution/bin/Isabelle;
20080702, by wenzelm
init_theory: pass name explicitly;
20080702, by wenzelm
replaced datatype category constructivism by is_theory/is_proof;
20080702, by wenzelm
Toplevel.init_theory: pass name explicitly;
20080702, by wenzelm
command: always keep transition, not just as initial status;
20080702, by wenzelm
cached code for code antiquotation
20080702, by haftmann
code antiquotation roaring ahead
20080702, by haftmann
cleaned up some code generator configuration
20080702, by haftmann
tuned;
20080701, by wenzelm
added datatype category;
20080701, by wenzelm
replaced datatype kind by OuterKeyword.category;
20080701, by wenzelm
clean: HOLPlain;
20080701, by wenzelm
prove lemma finite in context of finite class
20080701, by huffman
added HOLPlain;
20080701, by wenzelm
explicit identification of toplevel commands, with status etc.;
20080701, by wenzelm
added name_of;
20080701, by wenzelm
added get_id/put_id;
20080701, by wenzelm
(removed Complex/ROOT.ML)
20080701, by haftmann
HOL += HOLComplex
20080701, by haftmann
HOL += HOLComplex
20080701, by haftmann
tuned
20080701, by haftmann
HOL += HOLComplex
20080701, by haftmann
put file dependencies on separate lines
20080701, by huffman
range_composition no longer in simp set
20080701, by huffman
remove simp attribute from range_composition
20080701, by huffman
rename INF to INFM
20080701, by huffman
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
20080701, by huffman
remove redundant instance proof finite_po < cpo
20080701, by huffman
remove unused lemma is_lub_Iup'
20080701, by huffman
replace lub (range Y) with (LUB i. Y i)
20080701, by huffman
add file dependencies
20080701, by huffman
universal bifinite domain
20080701, by huffman
isomorphisms between naturals and sums, products, and finite sets
20080701, by huffman
theory of algebraic deflations
20080701, by huffman
theory of eventuallyconstant sequences
20080701, by huffman
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
20080701, by huffman
rename compact_approx to compact_take
20080701, by huffman
rename approx_pd to pd_take
20080701, by huffman
split Completion.thy from CompactBasis.thy
20080701, by huffman
filemap for CVS > Mercurial conversion;
20080630, by wenzelm
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
20080630, by huffman
New theory of deflations and embeddingprojection pairs
20080630, by huffman
remove unused Cset.thy
20080630, by huffman
added facts to lemma swap_simps and tuned lemma calc_atms
20080630, by urbanc
simplified retrieval of theory names of consts and types
20080630, by haftmann
tagged arities
20080630, by haftmann
HOLComplex with proof terms
20080630, by haftmann
code generator setup for "int" also works under etacontraction
20080630, by haftmann
less
more

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