Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Adding "ex/Induction_Scheme.thy" to tests
authorkrauss
Fri, 07 Dec 2007 10:59:03 +0100
changeset 25568 7bb10db582cf
parent 25567 5720345ea689
child 25569 c597835d5de4
Adding "ex/Induction_Scheme.thy" to tests
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/ex/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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 \
--- 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",
isabelle