src/HOLCF/Up.thy
2008-01-02 huffman 2008-01-02 remove not_up_less_UU [simp]
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2006-02-19 huffman 2006-02-19 use minimal imports
2005-11-30 huffman 2005-11-30 add xsymbol syntax for u type constructor
2005-11-03 huffman 2005-11-03 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
2005-10-12 huffman 2005-10-12 added compactness theorems
2005-09-22 huffman 2005-09-22 cleaned up
2005-07-28 wenzelm 2005-07-28 fixed var index in tactic;
2005-07-08 huffman 2005-07-08 define 'a u with datatype package; removed obsolete lemmas; renamed upE1 to upE and Exh_Up1 to Exh_Up; cleaned up
2005-06-23 huffman 2005-06-23 add csplit3, ssplit3, fup3 as simp rules
2005-06-08 huffman 2005-06-08 make up_eq and up_less into simp rules
2005-06-08 huffman 2005-06-08 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
2005-06-03 huffman 2005-06-03 changed to use new contlubI, etc.
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-03-10 huffman 2005-03-10 instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
2005-03-08 huffman 2005-03-08 reordered and arranged for document generation, cleaned up some proofs
2005-03-04 huffman 2005-03-04 fix headers
2005-03-04 huffman 2005-03-04 converted to new-style theories, and combined numbered files