# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260195711 -3600
# Node ID 0cf166548856c69c8fc6e5042f316228a89267c7
# Parent  7f35355df72e30e76c7494166dc26ade98b68975
isabelle make tests all examples

diff -r 7f35355df72e -r 0cf166548856 IsaMakefile
--- a/IsaMakefile	Mon Dec 07 15:18:44 2009 +0100
+++ b/IsaMakefile	Mon Dec 07 15:21:51 2009 +0100
@@ -13,7 +13,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf  ## -D generated
+USEDIR = $(ISABELLE_TOOL) usedir -v true -t true ## -D generated
 
 ## Quot
 
diff -r 7f35355df72e -r 0cf166548856 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 15:18:44 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 15:21:51 2009 +0100
@@ -1,9 +1,9 @@
 theory IntEx2
 imports "../QuotMain"
-uses
+(*uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
-  ("Tools/int_arith.ML")
+  ("Tools/int_arith.ML")*)
 begin
 
 
diff -r 7f35355df72e -r 0cf166548856 Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Mon Dec 07 15:18:44 2009 +0100
+++ b/Quot/Examples/LFex.thy	Mon Dec 07 15:21:51 2009 +0100
@@ -180,6 +180,8 @@
 where
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
+end
+
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
 lemma kpi_rsp[quotient_rsp]: 
   "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
@@ -299,9 +301,8 @@
 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 done
 
-print_quotients
-
 end
 
 
 
+
diff -r 7f35355df72e -r 0cf166548856 Quot/ROOT.ML
--- a/Quot/ROOT.ML	Mon Dec 07 15:18:44 2009 +0100
+++ b/Quot/ROOT.ML	Mon Dec 07 15:21:51 2009 +0100
@@ -1,8 +1,9 @@
-no_document use_thys 
+quick_and_dirty := true;
+
+no_document use_thys
    ["QuotMain",
     "Examples/Fset",
     "Examples/IntEx",
     "Examples/IntEx2",
     "Examples/LFex",
     "Examples/LamEx"];
-