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.
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
added ML/ml_thms.ML;
20080628, by wenzelm
tuned;
20080628, by wenzelm
tuned;
20080628, by wenzelm
additional ML antiquotations;
20080628, by wenzelm
moved theorem values to ml_thms.ML;
20080628, by wenzelm
Isar theorem values within ML.
20080628, by wenzelm
added ML/ml_thms.ML;
20080628, by wenzelm
updated generated file;
20080628, by wenzelm
allow overlap of minor keywords and commands;
20080628, by wenzelm
include HOLPlain;
20080628, by wenzelm
tuned args parser (cf. args.ML);
20080628, by wenzelm
replaced simple_text by fullyfeatured parse_args;
20080628, by wenzelm
tuned nested args parser;
20080628, by wenzelm
@{lemma}: 'by' keyword;
20080628, by wenzelm
ML: improved antiquotations;
20080628, by wenzelm
added macro interface;
20080628, by wenzelm
tuned;
20080628, by wenzelm
added thm_name, opt_thm_name;
20080628, by wenzelm
adjusted import
20080627, by haftmann
adjusted import
20080627, by haftmann
added a lemma to at_swap_simps
20080627, by urbanc
remove cset theory; define ideal completions using typedef instead of cpodef
20080626, by huffman
less
more

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