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