isabelle: Graph

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

cleaned up some code generator configuration
2008-07-02, by haftmann
tuned;
2008-07-01, by wenzelm
added datatype category;
2008-07-01, by wenzelm
replaced datatype kind by OuterKeyword.category;
2008-07-01, by wenzelm
clean: HOL-Plain;
2008-07-01, by wenzelm
prove lemma finite in context of finite class
2008-07-01, by huffman
added HOL-Plain;
2008-07-01, by wenzelm
explicit identification of toplevel commands, with status etc.;
2008-07-01, by wenzelm
added name_of;
2008-07-01, by wenzelm
added get_id/put_id;
2008-07-01, by wenzelm
(removed Complex/ROOT.ML)
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
tuned
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
put file dependencies on separate lines
2008-07-01, by huffman
range_composition no longer in simp set
2008-07-01, by huffman
remove simp attribute from range_composition
2008-07-01, by huffman
rename INF to INFM
2008-07-01, by huffman
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
2008-07-01, by huffman
remove redundant instance proof finite_po < cpo
2008-07-01, by huffman
remove unused lemma is_lub_Iup'
2008-07-01, by huffman
replace lub (range Y) with (LUB i. Y i)
2008-07-01, by huffman
add file dependencies
2008-07-01, by huffman
universal bifinite domain
2008-07-01, by huffman
isomorphisms between naturals and sums, products, and finite sets
2008-07-01, by huffman
theory of algebraic deflations
2008-07-01, by huffman
theory of eventually-constant sequences
2008-07-01, by huffman
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
2008-07-01, by huffman
rename compact_approx to compact_take
2008-07-01, by huffman
rename approx_pd to pd_take
2008-07-01, by huffman
split Completion.thy from CompactBasis.thy
2008-07-01, by huffman
filemap for CVS -> Mercurial conversion;
2008-06-30, by wenzelm
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
2008-06-30, by huffman
New theory of deflations and embedding-projection pairs
2008-06-30, by huffman
remove unused Cset.thy
2008-06-30, by huffman
added facts to lemma swap_simps and tuned lemma calc_atms
2008-06-30, by urbanc
simplified retrieval of theory names of consts and types
2008-06-30, by haftmann
tagged arities
2008-06-30, by haftmann
HOL-Complex with proof terms
2008-06-30, by haftmann
code generator setup for "int" also works under eta-contraction
2008-06-30, by haftmann
added ML/ml_thms.ML;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
additional ML antiquotations;
2008-06-28, by wenzelm
moved theorem values to ml_thms.ML;
2008-06-28, by wenzelm
Isar theorem values within ML.
2008-06-28, by wenzelm
added ML/ml_thms.ML;
2008-06-28, by wenzelm
updated generated file;
2008-06-28, by wenzelm
allow overlap of minor keywords and commands;
2008-06-28, by wenzelm
include HOL-Plain;
2008-06-28, by wenzelm
tuned args parser (cf. args.ML);
2008-06-28, by wenzelm
replaced simple_text by fully-featured parse_args;
2008-06-28, by wenzelm
tuned nested args parser;
2008-06-28, by wenzelm
@{lemma}: 'by' keyword;
2008-06-28, by wenzelm
ML: improved antiquotations;
2008-06-28, by wenzelm
added macro interface;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
added thm_name, opt_thm_name;
2008-06-28, by wenzelm
adjusted import
2008-06-27, by haftmann

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle