src/HOLCF/HOLCF.thy
author huffman
Sat Apr 02 00:33:51 2005 +0200 (2005-04-02)
changeset 15651 4b393520846e
parent 15650 b37dc98fbbc5
child 15742 64eae3513064
permissions -rw-r--r--
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
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@15650
     9
imports Sprod Ssum Up Lift Discrete One Tr
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