| author | huffman |
| Sat, 16 Apr 2005 00:17:52 +0200 | |
| changeset 15742 | 64eae3513064 |
| parent 15651 | 4b393520846e |
| child 16054 | b8ba6727712f |
| permissions | -rw-r--r-- |
| clasohm@1479 | 1 |
(* Title: HOLCF/HOLCF.thy |
| nipkow@243 | 2 |
ID: $Id$ |
| clasohm@1479 | 3 |
Author: Franz Regensburger |
| nipkow@243 | 4 |
|
| wenzelm@12030 | 5 |
Top theory for HOLCF system. |
| nipkow@243 | 6 |
*) |
| nipkow@243 | 7 |
|
| huffman@15650 | 8 |
theory HOLCF |
| huffman@15742 | 9 |
imports Sprod Ssum Up Lift Discrete One Tr Domain |
| huffman@15650 | 10 |
begin |
| huffman@15650 | 11 |
|
| huffman@15651 | 12 |
text {*
|
| huffman@15651 | 13 |
Remove continuity lemmas from simp set, so continuity subgoals |
| huffman@15651 | 14 |
are handled by the @{text cont_proc} simplifier procedure.
|
| huffman@15651 | 15 |
*} |
| huffman@15651 | 16 |
declare cont_lemmas1 [simp del] |
| huffman@15651 | 17 |
declare cont_lemmas_ext [simp del] |
| huffman@15651 | 18 |
|
| huffman@15650 | 19 |
end |