# HG changeset patch
# User oheimb
# Date 854726265 -3600
# Node ID b9f641195b484af1a84e8a2a1297bfaa6ec51ca1
# Parent  24d7e8fb8261ac89a2a54807b679be18a30e3f6a
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains

diff -r 24d7e8fb8261 -r b9f641195b48 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Fri Jan 31 16:56:32 1997 +0100
+++ b/src/HOLCF/IsaMakefile	Fri Jan 31 16:57:45 1997 +0100
@@ -32,8 +32,10 @@
 
 ## Miscellaneous examples
 
-EX_THYS = ex/Fix2.thy ex/Hoare.thy \
-	  ex/Loop.thy
+EX_THYS = ex/Classlib.thy ex/Witness.thy\
+	  ex/Dnat.thy ex/Dlist.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)
 
@@ -42,17 +44,16 @@
 
 
 ## Explicit domains
-
-EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
-			explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
-			explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy \
-			explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
+#
+#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\
+#		 explicit_domains/Dlist.thy \
+#		 explicit_domains/Stream.thy explicit_domains/Stream2.thy
 
-EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
-			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
-
-test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
+#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
+#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
+#
+#test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
+#	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
 
 
 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
diff -r 24d7e8fb8261 -r b9f641195b48 src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Fri Jan 31 16:56:32 1997 +0100
+++ b/src/HOLCF/Makefile	Fri Jan 31 16:57:45 1997 +0100
@@ -60,8 +60,10 @@
 $(BIN)/HOL:
 	cd ../HOL;  $(MAKE)
 
-EX_THYS =  ex/Fix2.thy ex/Hoare.thy \
-	   ex/Loop.thy	
+EX_THYS = ex/Classlib.thy ex/Witness.thy\
+	  ex/Dnat.thy ex/Dlist.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)
 
@@ -81,29 +83,29 @@
 			\"$(COMP)\" is not poly or sml;;\
 	esac
 
-EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
-			explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
-			explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy\
-			explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
+#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy \
+#		explicit_domains/Dlist.thy \
+#		explicit_domains/Stream.thy explicit_domains/Stream2.thy
 
-EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
-			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
+#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
+#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
 
-test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"explicit_domains";				  quit();' | $(COMP) $(BIN)/HOLCF;\
-		else echo 'exit_use_dir"explicit_domains"; quit();' \
-		       | $(COMP) $(BIN)/HOLCF;\
-		fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
-		       | $(BIN)/HOLCF;\
-		else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
+#test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
+#	@case `basename "$(COMP)"` in \
+#	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+#		then echo 'make_html := true; exit_use_dir"explicit_domains";\
+#			  quit();' | $(COMP) $(BIN)/HOLCF;\
+#		else echo 'exit_use_dir"explicit_domains"; quit();' \
+#		       | $(COMP) $(BIN)/HOLCF;\
+#		fi;;\
+#	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+#		then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
+#		       | $(BIN)/HOLCF;\
+#		else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
+#		fi;;\
+#	*)	echo Bad value for ISABELLECOMP: \
+#			\"$(COMP)\" is not poly or sml;;\
+#	esac
 
 .PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF