--- a/src/HOLCF/HOLCF.thy Mon Mar 22 15:05:20 2010 -0700
+++ b/src/HOLCF/HOLCF.thy Mon Mar 22 15:23:16 2010 -0700
@@ -11,7 +11,6 @@
Powerdomains
Sum_Cpo
uses
- "holcf_logic.ML"
"Tools/adm_tac.ML"
begin
--- a/src/HOLCF/IsaMakefile Mon Mar 22 15:05:20 2010 -0700
+++ b/src/HOLCF/IsaMakefile Mon Mar 22 15:23:16 2010 -0700
@@ -75,7 +75,6 @@
Tools/fixrec.ML \
Tools/pcpodef.ML \
Tools/repdef.ML \
- holcf_logic.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
--- a/src/HOLCF/Tools/holcf_library.ML Mon Mar 22 15:05:20 2010 -0700
+++ b/src/HOLCF/Tools/holcf_library.ML Mon Mar 22 15:23:16 2010 -0700
@@ -62,7 +62,6 @@
(*** Continuous function space ***)
-(* ->> is taken from holcf_logic.ML *)
fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
val (op ->>) = mk_cfunT;
--- a/src/HOLCF/holcf_logic.ML Mon Mar 22 15:05:20 2010 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* Title: HOLCF/holcf_logic.ML
- Author: David von Oheimb
-
-Abstract syntax operations for HOLCF.
-*)
-
-infixr 6 ->>;
-
-signature HOLCF_LOGIC =
-sig
- val mk_btyp: string -> typ * typ -> typ
- val pcpoS: sort
- val mk_TFree: string -> typ
- val cfun_arrow: string
- val ->> : typ * typ -> typ
- val mk_ssumT: typ * typ -> typ
- val mk_sprodT: typ * typ -> typ
- val mk_uT: typ -> typ
- val trT: typ
- val oneT: typ
-end;
-
-structure HOLCFLogic: HOLCF_LOGIC =
-struct
-
-(* sort pcpo *)
-
-val pcpoS = @{sort pcpo};
-fun mk_TFree s = TFree ("'" ^ s, pcpoS);
-
-
-(* basic types *)
-
-fun mk_btyp t (S, T) = Type (t, [S, T]);
-
-val cfun_arrow = @{type_name "cfun"};
-val op ->> = mk_btyp cfun_arrow;
-val mk_ssumT = mk_btyp (@{type_name "ssum"});
-val mk_sprodT = mk_btyp (@{type_name "sprod"});
-fun mk_uT T = Type (@{type_name u}, [T]);
-val trT = @{typ tr};
-val oneT = @{typ one};
-
-end;