# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260193030 -3600
# Node ID 81f40b8bde7bd7d3b88f2d05425377033d170292
# Parent  5d932e7a856cfd4002ff40339a6c937ec915fdd3
added "end" to each example theory

diff -r 5d932e7a856c -r 81f40b8bde7b IsaMakefile
--- a/IsaMakefile	Mon Dec 07 14:35:45 2009 +0100
+++ b/IsaMakefile	Mon Dec 07 14:37:10 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 5d932e7a856c -r 81f40b8bde7b Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 14:37:10 2009 +0100
@@ -274,3 +274,5 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* lambda_prs_tac  @{context} 1 *})
 sorry
+
+end
\ No newline at end of file
diff -r 5d932e7a856c -r 81f40b8bde7b Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 14:37:10 2009 +0100
@@ -434,3 +434,5 @@
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
 *)
+
+end
\ No newline at end of file
diff -r 5d932e7a856c -r 81f40b8bde7b Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Mon Dec 07 14:37:10 2009 +0100
@@ -250,3 +250,4 @@
   apply(simp add: var_supp)
   done
 
+end
\ No newline at end of file
diff -r 5d932e7a856c -r 81f40b8bde7b Quot/ROOT.ML
--- a/Quot/ROOT.ML	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/ROOT.ML	Mon Dec 07 14:37:10 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"];
+