author | wenzelm |
Tue, 17 May 2005 18:51:16 +0200 | |
changeset 15992 | cb02d70a2040 |
parent 15742 | 64eae3513064 |
child 16054 | b8ba6727712f |
permissions | -rw-r--r-- |
(* Title: HOLCF/HOLCF.thy ID: $Id$ Author: Franz Regensburger Top theory for HOLCF system. *) theory HOLCF imports Sprod Ssum Up Lift Discrete One Tr Domain begin text {* Remove continuity lemmas from simp set, so continuity subgoals are handled by the @{text cont_proc} simplifier procedure. *} declare cont_lemmas1 [simp del] declare cont_lemmas_ext [simp del] end