Fri, 03 Jun 2005 23:13:45 +0200 renamed to Ffun (full function space)
huffman [Fri, 03 Jun 2005 23:13:45 +0200] rev 16205
renamed to Ffun (full function space)
Fri, 03 Jun 2005 23:13:08 +0200 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman [Fri, 03 Jun 2005 23:13:08 +0200] rev 16204
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
Fri, 03 Jun 2005 22:21:43 +0200 added theorem ch2ch_lub
huffman [Fri, 03 Jun 2005 22:21:43 +0200] rev 16203
added theorem ch2ch_lub
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip