src/HOLCF/Lift.thy
Fri, 08 Jul 2005 03:09:32 +0200 huffman replaced old continuity rules with new lemma cont2cont_lift_case
Fri, 08 Jul 2005 02:42:04 +0200 huffman renamed upE1 to upE; added simp rule cont2cont_flift1
Thu, 07 Jul 2005 21:41:08 +0200 huffman removed obsolete continuity theorems
Thu, 07 Jul 2005 21:22:15 +0200 huffman define lift type using pcpodef; cleaned up
Tue, 05 Jul 2005 23:14:48 +0200 huffman simplified definitions of flift1, flift2, liftpair;
Fri, 01 Jul 2005 04:09:27 +0200 huffman added theorem lift_definedE; moved cont_if to Cont.thy
Thu, 23 Jun 2005 22:10:29 +0200 huffman add binder syntax for flift1
Tue, 14 Jun 2005 04:05:15 +0200 huffman renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
Fri, 03 Jun 2005 23:35:18 +0200 huffman renamed variable in cont2cont_app
Tue, 31 May 2005 11:53:12 +0200 wenzelm tuned;
Wed, 25 May 2005 02:49:46 +0200 huffman shorted proof that lift is chfin
Mon, 23 May 2005 23:24:38 +0200 huffman moved continuity simproc to Cont.thy
Fri, 06 May 2005 03:47:44 +0200 huffman Replaced all unnecessary uses of SOME with THE or LEAST
Sat, 02 Apr 2005 00:33:51 +0200 huffman Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
Fri, 04 Mar 2005 23:23:47 +0100 huffman fix headers
Fri, 04 Mar 2005 23:12:36 +0100 huffman converted to new-style theories, and combined numbered files
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Fri, 11 Jul 2003 13:54:26 +0200 oheimb corrected markup text
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Sat, 03 Nov 2001 01:38:11 +0100 wenzelm rep_datatype lift;
Mon, 17 Feb 1997 10:57:11 +0100 slotosch Changes of HOLCF from Oscar Slotosch:
less more (0) tip