src/HOLCF/Fixrec.thy
2009-11-02 huffman 2009-11-02 add fixrec support for HOL pair constructor patterns
2009-06-21 haftmann 2009-06-21 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-05-11 huffman 2009-05-11 simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
2009-04-27 huffman 2009-04-27 add proper support for bottom-patterns in fixrec package
2009-04-20 huffman 2009-04-20 fix too-specific types in lemmas match_{sinl,sinr}_simps
2009-04-11 huffman 2009-04-11 change definition of match combinators for fixrec package
2009-02-26 huffman 2009-02-26 use TheoryData to keep track of pattern match combinators
2009-01-14 huffman 2009-01-14 change to simpler, more extensible continuity simproc define attribute [cont2cont] for continuity rules; new continuity simproc just applies cont2cont rules repeatedly; split theory Product_Cpo from Cprod, so Cfun can import Product_Cpo; add lemma cont2cont_LAM', which is suitable as a cont2cont rule.
2009-01-02 wenzelm 2009-01-02 renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;
2008-12-18 huffman 2008-12-18 constdefs -> definition
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-12-11 wenzelm 2008-12-11 pcpodef package: state two goals, instead of encoded conjunction;
2008-11-25 huffman 2008-11-25 separate run and cases combinators
2008-02-07 huffman 2008-02-07 fix broken syntax translations
2007-10-23 wenzelm 2007-10-23 translations: use XCONST for input patterns (keeps original spelling of const);
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2007-05-31 wenzelm 2007-05-31 moved HOLCF tools to canonical place;
2006-04-13 huffman 2006-04-13 hide common name of constant 'run'
2006-04-10 wenzelm 2006-04-10 hide (open) const;
2006-03-24 huffman 2006-03-24 lazy patterns in lambda abstractions
2006-02-19 huffman 2006-02-19 use qualified name for return
2006-02-17 huffman 2006-02-17 make maybe into a real type constructor; remove monad syntax
2005-11-30 huffman 2005-11-30 reimplement Case expression pattern matching to support lazy patterns
2005-11-07 huffman 2005-11-07 reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
2005-11-07 huffman 2005-11-07 remove syntax for as-patterns
2005-11-06 huffman 2005-11-06 add case syntax stuff
2005-11-06 huffman 2005-11-06 use consts for infix syntax
2005-11-05 huffman 2005-11-05 simplify definitions
2005-07-12 huffman 2005-07-12 changed orientation of bind_assoc rule
2005-07-12 huffman 2005-07-12 generalized types of monadic operators to class cpo; added match function for UU
2005-07-08 huffman 2005-07-08 fix typo
2005-07-08 huffman 2005-07-08 renamed upE1 to upE
2005-06-23 huffman 2005-06-23 added match functions for spair, sinl, sinr
2005-06-18 huffman 2005-06-18 fixrec shows unsolved subgoals when proofs of rewrites fail
2005-06-17 huffman 2005-06-17 added match functions for ONE, TT, and FF; added theorem mplus_fail2
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-15 huffman 2005-06-15 fixrec package now handles mutually-recursive definitions
2005-06-04 huffman 2005-06-04 use fixrec_package.ML
2005-06-04 huffman 2005-06-04 New theory with lemmas for the fixrec package