--- 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
--- 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)
- ]);
--- 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
--- 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";