src/HOLCF/Fixrec.thy
2010-11-27 huffman 2010-11-27 rename function 'match_UU' to 'match_bottom'
2010-11-27 huffman 2010-11-27 rename function 'strict' to 'seq', which is its name in Haskell
2010-11-26 huffman 2010-11-26 remove case combinator for fixrec match type
2010-11-10 huffman 2010-11-10 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-10-29 huffman 2010-10-29 renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
2010-10-27 huffman 2010-10-27 make syntax of continuous if-then-else consistent with HOL if-then-else
2010-10-20 huffman 2010-10-20 introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
2010-09-30 huffman 2010-09-30 fixrec: rename match_cpair to match_Pair
2010-05-24 huffman 2010-05-24 move unused pattern match syntax stuff into HOLCF/ex
2010-05-24 huffman 2010-05-24 rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
2010-05-22 huffman 2010-05-22 remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
2010-05-22 huffman 2010-05-22 remove cont2cont simproc; instead declare cont2cont rules as simp rules
2010-05-19 huffman 2010-05-19 remove unnecessary constant Fixrec.bind
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-23 huffman 2010-03-23 minimize dependencies
2010-03-22 huffman 2010-03-22 completely remove constants cpair, cfst, csnd
2010-03-22 huffman 2010-03-22 remove unused syntax for as_pat, lazy_pat
2010-03-02 huffman 2010-03-02 fixrec and repdef modules import holcf_library
2010-02-28 huffman 2010-02-28 fix output translation for Case syntax
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-11-03 huffman 2009-11-03 add more fixrec_simp rules
2009-11-03 huffman 2009-11-03 add fixrec_simp attribute and method (eventually to replace fixpat)
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