2010-03-04 ago wenzelm point to http://hginit.com/
2010-03-04 ago paulson Simplified a couple of proofs and corrected a comment
2010-03-04 ago haftmann lemmas set_map_of_compr, map_of_inject_set
2010-03-03 ago huffman merged
2010-03-03 ago huffman merged
2010-03-03 ago huffman remove dead code
2010-03-03 ago huffman add infix declarations
2010-03-03 ago huffman remove unnecessary theorem references
2010-03-03 ago huffman remove copy_of_dtyp from domain_axioms.ML
2010-03-03 ago huffman add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
2010-03-03 ago huffman uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
2010-03-03 ago huffman add function axiomatize_lub_take
2010-03-03 ago huffman move function mk_lub into holcf_library.ML
2010-03-03 ago wenzelm added extern_syntax;
2010-03-03 ago haftmann merged
2010-03-03 ago haftmann more uniform naming conventions
2010-03-03 ago haftmann tuned whitespace
2010-03-03 ago haftmann restructured RBT theory
2010-03-03 ago wenzelm stats for at-poly-test;
2010-03-03 ago wenzelm proper names for types cfun, sprod, ssum (cf. fa231b86cb1e);
2010-03-03 ago wenzelm merged, resolving some basic conflicts;
2010-03-03 ago krauss merged
2010-03-03 ago krauss updated patch for hgweb style: now applies to Mercurial 1.4.3 templates
2010-03-03 ago krauss fix fragile proof using old induction rule (cf. bdf8ad377877)
2010-03-03 ago hoelzl merged
2010-03-02 ago himmelma replaced \<bullet> with inner
2010-03-02 ago himmelma tuned
2010-03-02 ago himmelma the ordering on real^1 is linear
2010-03-03 ago bulwahn merged
2010-03-02 ago bulwahn made smlnj happy
2010-03-02 ago bulwahn adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
2010-03-02 ago bulwahn adding HOL-Mutabelle to tests
2010-03-03 ago haftmann merged
2010-03-03 ago haftmann more explicit naming scheme
2010-03-02 ago huffman merged
2010-03-02 ago huffman adapt to changed variable name in casedist theorem
2010-03-02 ago huffman remove dependency on domain_syntax.ML
2010-03-02 ago huffman update HOLCF makefile
2010-03-02 ago huffman simplify add_axioms function; remove obsolete domain_syntax.ML
2010-03-02 ago huffman proof scripts use variable name y for casedist
2010-03-02 ago huffman fixrec and repdef modules import holcf_library
2010-03-02 ago huffman use y as variable name in casedist, like datatype package
2010-03-02 ago huffman proper names for types cfun, sprod, ssum
2010-03-02 ago huffman variable name changed
2010-03-02 ago huffman fix proof script for take_apps so it works with indirect recursion
2010-03-02 ago huffman remove dead code
2010-03-02 ago huffman remove unused mixfix component from type cons
2010-03-02 ago huffman cleaned up, added type annotations
2010-03-02 ago huffman remove unused selector field from type arg
2010-03-02 ago huffman add_syntax no longer needs a definitional mode
2010-03-02 ago huffman add_axioms no longer needs a definitional mode
2010-03-02 ago huffman get rid of primes on thy variables
2010-03-02 ago huffman move definition of finiteness predicate into domain_take_proofs.ML
2010-03-02 ago huffman move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-02 ago huffman remove map_tab argument to calc_axioms
2010-03-02 ago huffman remove dead code
2010-03-02 ago paulson merged
2010-03-02 ago paulson Slightly generalised a theorem
2010-03-02 ago paulson merged
2010-02-19 ago paulson merged