# HG changeset patch
# User wenzelm
# Date 877344351 -7200
# Node ID d52a49a7d8f3a11c2b454821f36be1882ad9da99
# Parent  e9d5bcae8351789413d575a8d242aa0a75abea1f
removed Dlist;

diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Mon Oct 20 11:53:42 1997 +0200
+++ b/src/HOLCF/IsaMakefile	Mon Oct 20 12:45:51 1997 +0200
@@ -89,6 +89,7 @@
 IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
 
+
 ## IMP
 
 IMP_THYS = IMP/Denotational.thy
@@ -97,20 +98,23 @@
 IMP:	$(OUT)/HOLCF $(IMP_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
 
+
 ## Miscellaneous examples
 
-EX_THYS = ex/Dnat.thy ex/Dlist.thy ex/Stream.thy \
+EX_THYS = ex/Dnat.thy ex/Stream.thy \
 	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \
 	  ex/Hoare.thy ex/Loop.thy
 
 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
 
-EX:	ex/ROOT.ML $(EX_FILES)
+ex:	ex/ROOT.ML $(EX_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOLCF ex
 
+
 ## Full test
 
-test:	$(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX
+test:	$(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP ex
 	echo 'Test examples ran successfully' > test
 
+
 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/ex/Dlist.ML
--- a/src/HOLCF/ex/Dlist.ML	Mon Oct 20 11:53:42 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-open Dlist;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties of lmap                                     *)
-(* ------------------------------------------------------------------------- *)
-
-bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def 
-        "lmap = (LAM f s. case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
-
-(* ------------------------------------------------------------------------- *)
-(* recursive  properties   of lmap                                           *)
-(* ------------------------------------------------------------------------- *)
-
-qed_goal "lmap1" Dlist.thy "lmap`f`UU = UU"
- (fn prems =>
-	[
-	(rtac (lmap_def2 RS ssubst) 1),
-	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
-	]);
-
-qed_goal "lmap2" Dlist.thy "lmap`f`dnil = dnil"
- (fn prems =>
-	[
-	(rtac (lmap_def2 RS ssubst) 1),
-	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
-	]);
-
-qed_goal "lmap3" Dlist.thy 
-	"[|x~=UU; xs~=UU|] ==> lmap`f`(x##xs) = (f`x)##(lmap`f`xs)"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac trans 1),
-	(rtac (lmap_def2 RS ssubst) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist.rews) 1),
-	(rtac refl 1)
-	]);
diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/ex/Dlist.thy
--- a/src/HOLCF/ex/Dlist.thy	Mon Oct 20 11:53:42 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      HOLCF/Dlist.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
-*)
-
-Dlist = Classlib +
-
-domain 'a dlist = dnil | "##" (dhd::'a) (dtl::'a dlist) (cinfixr 65)
-
-
-consts
-
-lmap	:: "('a -> 'b) -> 'a dlist -> 'b dlist"
-lmem	:: "('a::eq)  -> 'a dlist -> tr"
-
-defs
-
-lmap_def "lmap == fix`(LAM h f s. case s of dnil => dnil
-			          | x ## xs => f`x ## h`f`xs)"
-
-lmem_def "lmem == fix`(LAM h e l. case l of dnil => FF
-     	 	  		  | x ## xs => If e Ù x then TT else h`e`xs fi)"
-
-end
diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Mon Oct 20 11:53:42 1997 +0200
+++ b/src/HOLCF/ex/ROOT.ML	Mon Oct 20 12:45:51 1997 +0200
@@ -11,9 +11,7 @@
 writeln"Root file for HOLCF examples";
 proof_timing := true;
 
-time_use_thy "Classlib";
 time_use_thy "Dnat";
-time_use_thy "Dlist";
 time_use_thy "Stream";
 time_use_thy "Dagstuhl";
 time_use_thy "Focus_ex";