Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
authorwenzelm
Tue, 25 May 2010 22:12:26 +0200
changeset 37119 b36a5512c5fb
parent 37118 ccae4ecd67f4
child 37120 5df087c6ce94
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
src/HOLCF/IsaMakefile file | annotate | diff | comparison | revisions
src/HOLCF/Library/HOLCF_Library_ROOT.ML file | annotate | diff | comparison | revisions
src/HOLCF/Library/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/IsaMakefile	Tue May 25 21:49:44 2010 +0200
+++ b/src/HOLCF/IsaMakefile	Tue May 25 22:12:26 2010 +0200
@@ -101,8 +101,8 @@
   Library/Strict_Fun.thy \
   Library/Sum_Cpo.thy \
   Library/HOLCF_Library.thy \
-  Library/ROOT.ML
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
+  Library/HOLCF_Library_ROOT.ML
+	@$(ISABELLE_TOOL) usedir -f HOLCF_Library_ROOT.ML $(OUT)/HOLCF Library
 
 
 ## HOLCF-IMP
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Library/HOLCF_Library_ROOT.ML	Tue May 25 22:12:26 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["HOLCF_Library"];
--- a/src/HOLCF/Library/ROOT.ML	Tue May 25 21:49:44 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["HOLCF_Library"];
isabelle