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.
modernized session ROOT setup;
authorwenzelm
Mon, 06 Sep 2010 13:22:11 +0200
changeset 39156 b4f18ac786fa
parent 39155 3e94ebe282f1
child 39157 b98909faaea8
modernized session ROOT setup;
src/HOL/Import/HOL/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Unix/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/HOL/ROOT.ML	Mon Sep 06 13:06:27 2010 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Mon Sep 06 13:22:11 2010 +0200
@@ -1,4 +1,2 @@
-
 use_thy "~~/src/HOL/Old_Number_Theory/Primes";
-setmp_noncritical quick_and_dirty true use_thy "HOL4Prob";
-setmp_noncritical quick_and_dirty true use_thy "HOL4";
+setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];
--- a/src/HOL/IsaMakefile	Mon Sep 06 13:06:27 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 06 13:22:11 2010 +0200
@@ -785,7 +785,7 @@
 $(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy		\
   Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy			\
   Unix/document/root.bib Unix/document/root.tex
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
+	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
 
 
 ## HOL-ZF
--- a/src/HOL/Unix/ROOT.ML	Mon Sep 06 13:06:27 2010 +0200
+++ b/src/HOL/Unix/ROOT.ML	Mon Sep 06 13:22:11 2010 +0200
@@ -1,2 +1,1 @@
-setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
-  use_thys ["Unix"];
+use_thys ["Unix"];
isabelle