# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260195524 -3600
# Node ID 7f35355df72e30e76c7494166dc26ade98b68975
# Parent  e56eeb9fedb36b4078882ed898e46e35ae2d5a49# Parent  81f40b8bde7bd7d3b88f2d05425377033d170292
merge

diff -r e56eeb9fedb3 -r 7f35355df72e IsaMakefile
--- a/IsaMakefile	Mon Dec 07 15:18:00 2009 +0100
+++ b/IsaMakefile	Mon Dec 07 15:18:44 2009 +0100
@@ -3,9 +3,8 @@
 
 default: Quot
 images: 
-test: Quot
 
-all: images test
+all: Quot
 
 
 ## global settings
@@ -16,13 +15,12 @@
 
 USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf  ## -D generated
 
-
 ## Quot
 
 Quot: $(LOG)/HOL-Quot.gz
 
 $(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy
-	@$(USEDIR) HOL Quot
+	@$(USEDIR) HOL-Nominal Quot
 
 
 ## clean
diff -r e56eeb9fedb3 -r 7f35355df72e Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Dec 07 15:18:00 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 15:18:44 2009 +0100
@@ -272,3 +272,5 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
 sorry
+
+end
\ No newline at end of file
diff -r e56eeb9fedb3 -r 7f35355df72e Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 15:18:00 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 15:18:44 2009 +0100
@@ -434,3 +434,5 @@
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
 *)
+
+end
\ No newline at end of file
diff -r e56eeb9fedb3 -r 7f35355df72e Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Mon Dec 07 15:18:00 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Mon Dec 07 15:18:44 2009 +0100
@@ -250,3 +250,4 @@
   apply(simp add: var_supp)
   done
 
+end
\ No newline at end of file
diff -r e56eeb9fedb3 -r 7f35355df72e Quot/ROOT.ML
--- a/Quot/ROOT.ML	Mon Dec 07 15:18:00 2009 +0100
+++ b/Quot/ROOT.ML	Mon Dec 07 15:18:44 2009 +0100
@@ -1,4 +1,8 @@
-(*
-  no_document use_thys ["This_Theory1", "This_Theory2"];
-  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
-*)
+no_document use_thys 
+   ["QuotMain",
+    "Examples/Fset",
+    "Examples/IntEx",
+    "Examples/IntEx2",
+    "Examples/LFex",
+    "Examples/LamEx"];
+