isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

merged
2010-03-05, by wenzelm
fix proof script so 'domain foo = Foo foo' works
2010-03-05, by huffman
fix proof script so qdomain_isomorphism foo = foo' works
2010-03-05, by huffman
finish browser_info: invoke isabelle browser -b to ensure that the jar really exists;
2010-03-05, by wenzelm
isabelle browser -b: Admin/build only;
2010-03-05, by wenzelm
merged
2010-03-05, by huffman
skip proof of induction rule for indirect-recursive domain definitions
2010-03-05, by huffman
generalized inj_uminus; added strict_mono_imp_inj_on
2010-03-05, by hoelzl
merged
2010-03-05, by hoelzl
Add Lebesgue integral and probability space.
2010-03-04, by hoelzl
Supremum and Infimum on real intervals
2010-03-04, by hoelzl
Rewrite rules for images of minus of intervals
2010-03-04, by hoelzl
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
2010-03-04, by hoelzl
Added natfloor and floor rules for multiplication and power.
2010-03-04, by hoelzl
Generalized setsum_cases
2010-03-04, by hoelzl
Added vimage_inter_cong
2010-03-04, by hoelzl
merged
2010-03-04, by huffman
move coinduction-related stuff into function prove_coindunction
2010-03-04, by huffman
add function add_qualified_simp_thm
2010-03-04, by huffman
generate lemma take_below, declare chain_take [simp]
2010-03-03, by huffman
switch to polyml-svn;
2010-03-04, by wenzelm
basic simplification of external_prover signature;
2010-03-04, by wenzelm
tuned;
2010-03-04, by wenzelm
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
2010-03-04, by wenzelm
point to http://hginit.com/
2010-03-04, by wenzelm
Simplified a couple of proofs and corrected a comment
2010-03-04, by paulson
lemmas set_map_of_compr, map_of_inject_set
2010-03-04, by haftmann
merged
2010-03-03, by huffman
merged
2010-03-03, by huffman
remove dead code
2010-03-03, by huffman
add infix declarations
2010-03-03, by huffman
remove unnecessary theorem references
2010-03-03, by huffman
remove copy_of_dtyp from domain_axioms.ML
2010-03-03, by huffman
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
2010-03-03, by huffman
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
2010-03-03, by huffman
add function axiomatize_lub_take
2010-03-03, by huffman
move function mk_lub into holcf_library.ML
2010-03-03, by huffman
added extern_syntax;
2010-03-03, by wenzelm
merged
2010-03-03, by haftmann
more uniform naming conventions
2010-03-03, by haftmann
tuned whitespace
2010-03-03, by haftmann
restructured RBT theory
2010-03-03, by haftmann
stats for at-poly-test;
2010-03-03, by wenzelm
proper names for types cfun, sprod, ssum (cf. fa231b86cb1e);
2010-03-03, by wenzelm
merged, resolving some basic conflicts;
2010-03-03, by wenzelm
merged
2010-03-03, by krauss
updated patch for hgweb style: now applies to Mercurial 1.4.3 templates
2010-03-03, by krauss
fix fragile proof using old induction rule (cf. bdf8ad377877)
2010-03-03, by krauss
merged
2010-03-03, by hoelzl
replaced \<bullet> with inner
2010-03-02, by himmelma
tuned
2010-03-02, by himmelma
the ordering on real^1 is linear
2010-03-02, by himmelma
merged
2010-03-03, by bulwahn
made smlnj happy
2010-03-02, by bulwahn
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
2010-03-02, by bulwahn
adding HOL-Mutabelle to tests
2010-03-02, by bulwahn
merged
2010-03-03, by haftmann
more explicit naming scheme
2010-03-03, by haftmann
merged
2010-03-02, by huffman
adapt to changed variable name in casedist theorem
2010-03-02, by huffman

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

isabelle