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

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
remove dependency on domain_syntax.ML
2010-03-02, by huffman
update HOLCF makefile
2010-03-02, by huffman
simplify add_axioms function; remove obsolete domain_syntax.ML
2010-03-02, by huffman
proof scripts use variable name y for casedist
2010-03-02, by huffman
fixrec and repdef modules import holcf_library
2010-03-02, by huffman
use y as variable name in casedist, like datatype package
2010-03-02, by huffman
proper names for types cfun, sprod, ssum
2010-03-02, by huffman
variable name changed
2010-03-02, by huffman
fix proof script for take_apps so it works with indirect recursion
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
remove unused mixfix component from type cons
2010-03-02, by huffman
cleaned up, added type annotations
2010-03-02, by huffman
remove unused selector field from type arg
2010-03-02, by huffman
add_syntax no longer needs a definitional mode
2010-03-02, by huffman
add_axioms no longer needs a definitional mode
2010-03-02, by huffman
get rid of primes on thy variables
2010-03-02, by huffman
move definition of finiteness predicate into domain_take_proofs.ML
2010-03-02, by huffman

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

isabelle