# HG changeset patch
# User wenzelm
# Date 924277562 -7200
# Node ID 931fc1daa8b1b987db7e8b1180c3dc1e78fa2865
# Parent  2ebe9e630cab50e55dd52a35bdd5af7d0b359ae8
added Isar_examples;

diff -r 2ebe9e630cab -r 931fc1daa8b1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 16 17:44:29 1999 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 16 17:46:02 1999 +0200
@@ -11,7 +11,9 @@
 test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Real \
   HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
   HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
-  HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory
+  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
+  TLA-Buffer TLA-Memory
+
 all: images test
 
 
@@ -312,6 +314,16 @@
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 
+## HOL-Isar_examples
+
+HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
+
+$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
+  Isar_examples/Cantor.thy Isar_examples/ExprCompiler.thy \
+  Isar_examples/Peirce.thy Isar_examples/ROOT.ML
+	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
+
+
 ## TLA
 
 TLA: HOL $(OUT)/TLA
@@ -367,5 +379,6 @@
 	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
 	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
 	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
-	  $(LOG)/HOL-ex.gz $(OUT)/TLA $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz \
-	  $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
+	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
+	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
+	  $(LOG)/TLA-Memory.gz