--- a/src/HOL/IsaMakefile Thu Jun 21 12:01:27 2007 +0200
+++ b/src/HOL/IsaMakefile Thu Jun 21 13:23:33 2007 +0200
@@ -27,6 +27,7 @@
HOL-Isar_examples \
HOL-Lambda \
HOL-Lattice \
+ HOL-MetisExamples \
HOL-MicroJava \
HOL-Modelcheck \
HOL-NanoJava \
@@ -390,6 +391,18 @@
@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
+## HOL-MetisExamples
+
+HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz
+
+$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL \
+ MetisExamples/ROOT.ML \
+ MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \
+ MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \
+ MetisExamples/set.thy
+ @$(ISATOOL) usedir -g true $(OUT)/HOL MetisExamples
+
+
## HOL-Algebra
HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz