# HG changeset patch
# User krauss
# Date 1197021543 -3600
# Node ID 7bb10db582cfb3dd909037483078bc2e64859451
# Parent  5720345ea689d0cb35c5d16b3e1346dafb3ca922
Adding "ex/Induction_Scheme.thy" to tests

diff -r 5720345ea689 -r 7bb10db582cf src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Dec 07 09:42:20 2007 +0100
+++ b/src/HOL/IsaMakefile	Fri Dec 07 10:59:03 2007 +0100
@@ -676,6 +676,7 @@
   ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
   ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
   ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
+	ex/Induction_Scheme.thy \
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
   ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \
   ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
diff -r 5720345ea689 -r 7bb10db582cf src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Dec 07 09:42:20 2007 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Dec 07 10:59:03 2007 +0100
@@ -24,6 +24,7 @@
   "Binary",
   "Recdefs",
   "Fundefs",
+  "Induction_Scheme",
   "InductiveInvariant_examples",
   "Locales",
   "LocaleTest2",