# HG changeset patch
# User haftmann
# Date 1284382442 -7200
# Node ID c1f3992c90975b69a180e21df4b0adf7e49b5892
# Parent  d4fa19eb082265cfe98227999d009230e0162e5c
print mode for Imperative HOL overview; tuned and more accurate dependencies

diff -r d4fa19eb0822 -r c1f3992c9097 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 13 14:53:56 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 13 14:54:02 2010 +0200
@@ -787,7 +787,7 @@
 
 HOL-ZF: HOL $(LOG)/HOL-ZF.gz
 
-$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy	\
+$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
   ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
 
@@ -796,18 +796,23 @@
 
 HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
 
-$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy	\
-  Imperative_HOL/Heap.thy Imperative_HOL/Heap_Monad.thy			\
-  Imperative_HOL/Imperative_HOL.thy Imperative_HOL/Imperative_HOL_ex.thy\
-  Imperative_HOL/Mrec.thy Imperative_HOL/Ref.thy			\
-  Imperative_HOL/ex/Imperative_Quicksort.thy				\
-  Imperative_HOL/ex/Imperative_Reverse.thy				\
-  Imperative_HOL/ex/Linked_Lists.thy					\
-  Imperative_HOL/ex/SatChecker.thy					\
-  Imperative_HOL/ex/Sorted_List.thy					\
-  Imperative_HOL/ex/Subarray.thy					\
+$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \
+  Imperative_HOL/Array.thy \
+  Imperative_HOL/Heap.thy \
+  Imperative_HOL/Heap_Monad.thy \
+  Imperative_HOL/Imperative_HOL.thy \
+  Imperative_HOL/Imperative_HOL_ex.thy \
+  Imperative_HOL/Mrec.thy \
+  Imperative_HOL/Ref.thy \
+  Imperative_HOL/ROOT.ML \
+  Imperative_HOL/ex/Imperative_Quicksort.thy \
+  Imperative_HOL/ex/Imperative_Reverse.thy \
+  Imperative_HOL/ex/Linked_Lists.thy \
+  Imperative_HOL/ex/SatChecker.thy \
+  Imperative_HOL/ex/Sorted_List.thy \
+  Imperative_HOL/ex/Subarray.thy \
   Imperative_HOL/ex/Sublist.thy
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
+	@$(ISABELLE_TOOL) usedir -g true -m iff -m no_brackets $(OUT)/HOL Imperative_HOL
 
 
 ## HOL-Decision_Procs