2006-07-04 berghofe 2006-07-04 Implemented proofs of equivariance and finite support for graph of recursion combinator.
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-07-04 urbanc 2006-07-04 updated
2006-07-04 ballarin 2006-07-04 Typo.
2006-07-04 ballarin 2006-07-04 Minor new lemmas.
2006-07-03 nipkow 2006-07-03 replaced respects2 by congruent2 because of type problem
2006-07-03 nipkow 2006-07-03 replaced translation by abbreviation
2006-07-03 wenzelm 2006-07-03 obtain_export: Thm.generalize; guess: fixed handling of mixfixes of vars; tuned;
2006-07-03 wenzelm 2006-07-03 project_algebra: norm_sort; tuned;
2006-07-03 webertj 2006-07-03 comments fixed, minor optimization wrt. certifying terms
2006-07-03 dixon 2006-07-03 fix to subst in order to allow subst when head of a term is a bound variable.
2006-07-03 webertj 2006-07-03 CNF tactic invocations moved into comments
2006-07-03 webertj 2006-07-03 comment added
2006-07-02 urbanc 2006-07-02 added more infrastructure for the recursion combinator
2006-06-30 nipkow 2006-06-30 normal_form to lemma test
2006-06-30 nipkow 2006-06-30 normalization uses refl now
2006-06-30 mengj 2006-06-30 Removed some incorrect axioms.
2006-06-30 haftmann 2006-06-30 fixed stale theory bug
2006-06-30 haftmann 2006-06-30 slight refinements
2006-06-30 haftmann 2006-06-30 refinement in instance command
2006-06-30 haftmann 2006-06-30 small change in class_package
2006-06-29 paulson 2006-06-29 added the "th" field to datatype Clause
2006-06-29 paulson 2006-06-29 fixed the "factor" method
2006-06-29 nipkow 2006-06-29 new function norm_term
2006-06-29 nipkow 2006-06-29 new method "normalization"
2006-06-29 kleing 2006-06-29 use -f in cp to overwrite read-only files (e.g. .svn in document/)
2006-06-28 webertj 2006-06-28 world map now transparent
2006-06-28 haftmann 2006-06-28 improvements in Classpackage
2006-06-28 haftmann 2006-06-28 reduced code, better instance command
2006-06-28 haftmann 2006-06-28 slight improvements in code generation
2006-06-28 haftmann 2006-06-28 added lookup function for parameters
2006-06-28 paulson 2006-06-28 disjunctive wellfoundedness
2006-06-27 haftmann 2006-06-27 class package refinements, slight code generation refinements
2006-06-27 haftmann 2006-06-27 added class projection
2006-06-27 haftmann 2006-06-27 slight improvement
2006-06-27 haftmann 2006-06-27 replaced subgraph by project
2006-06-24 wenzelm 2006-06-24 fix/fixes: tuned type constraints;
2006-06-24 wenzelm 2006-06-24 minor tuning of definitions/proofs;
2006-06-24 wenzelm 2006-06-24 fixed translations for _MapUpd: CONST;
2006-06-23 nipkow 2006-06-23 beautification
2006-06-23 haftmann 2006-06-23 added webmaster
2006-06-23 paulson 2006-06-23 Introduction of Ramsey's theorem
2006-06-22 ballarin 2006-06-22 Removed debugging code.
2006-06-22 ballarin 2006-06-22 Improved handling of defines imported in duplicate.
2006-06-22 kleing 2006-06-22 new standard dir structure
2006-06-21 webertj 2006-06-21 world map updated
2006-06-21 webertj 2006-06-21 world map updated
2006-06-21 krauss 2006-06-21 Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command
2006-06-21 haftmann 2006-06-21 fixed bug resolving Haskell names
2006-06-21 haftmann 2006-06-21 fixed error bug
2006-06-21 haftmann 2006-06-21 renamed thy data
2006-06-21 krauss 2006-06-21 Added split_cong rule
2006-06-21 haftmann 2006-06-21 hyps better than prems
2006-06-20 haftmann 2006-06-20 fixed sml/nj value restriction problem
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-20 krauss 2006-06-20 Fixed another variable order bug...
2006-06-20 haftmann 2006-06-20 switched to open locales for classes
2006-06-20 haftmann 2006-06-20 switched to open locales for classes
2006-06-19 wenzelm 2006-06-19 refrain from reforming TFL -- back to previous revision;
2006-06-19 wenzelm 2006-06-19 added declare_thm, thm_context; added trade(T);