# HG changeset patch
# User huffman
# Date 1269296596 25200
# Node ID e0382e4b4da79a09a2ea41a5009148f521bd0393
# Parent  3d699b736ff4ca63e29718f5e8d22708e97368f9
remove obsolete holcf_logic.ML

diff -r 3d699b736ff4 -r e0382e4b4da7 src/HOLCF/HOLCF.thy
--- 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
 
diff -r 3d699b736ff4 -r e0382e4b4da7 src/HOLCF/IsaMakefile
--- 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
 
diff -r 3d699b736ff4 -r e0382e4b4da7 src/HOLCF/Tools/holcf_library.ML
--- 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;
diff -r 3d699b736ff4 -r e0382e4b4da7 src/HOLCF/holcf_logic.ML
--- 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;