--- a/src/HOL/HOLCF/Fixrec.thy Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy Tue Apr 04 21:57:43 2017 +0200
@@ -5,7 +5,7 @@
section "Package for defining recursive functions in HOLCF"
theory Fixrec
-imports Plain_HOLCF
+imports Cprod Sprod Ssum Up One Tr Fix
keywords "fixrec" :: thy_decl
begin
@@ -139,7 +139,7 @@
match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where
"match_TT = (\<Lambda> x k. If x then k else fail)"
-
+
definition
match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where