# HG changeset patch
# User mehta
# Date 1081260639 -7200
# Node ID 0ccba84113a1553743051e806fa5177a99c28c0b
# Parent  5656e3151f1799cbcf262092c1c32529561bc22f
*** empty log message ***

diff -r 5656e3151f17 -r 0ccba84113a1 doc-src/Exercises/2003/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/IsaMakefile	Tue Apr 06 16:10:39 2004 +0200
@@ -0,0 +1,76 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV2003
+#
+
+SESSIONS = a1 a2 a3 a5 a6
+
+## targets
+
+default: clean sessions
+sessions: $(SESSIONS)
+# all: sessions 
+
+
+## global settings
+
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+INFO = $(ISABELLE_BROWSER_INFO)
+USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated
+RSYNC = rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync
+WWW = www4.in.tum.de:/home/html/wbroy/html-data/lehre/praktika/psv
+
+
+# reomve old log files
+clean:
+	rm -f $(LOG)/HOL-a?.gz $(LOG)/HOL-l?.gz
+
+## provide style.tex
+
+style:
+	@for D in $(SESSIONS); do test -d $$D/document && { test -r $$D/document/style.tex || ln -s ../../style.tex $$D/document/style.tex; } done;
+
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML \
+  a1/*.thy
+	@$(USEDIR) HOL a1
+
+## a2
+
+a2: a2/generated/session.tex
+
+a2/generated/session.tex: a2/ROOT.ML \
+  a2/*.thy
+	@$(USEDIR) HOL a2
+
+## a3
+
+a3: a3/generated/session.tex
+
+a3/generated/session.tex: a3/ROOT.ML \
+  a3/*.thy
+	@$(USEDIR) HOL a3
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML \
+  a5/*.thy
+	@$(USEDIR) HOL a5
+
+## a6
+
+ a6: a6/generated/session.tex
+
+ a6/generated/session.tex: a6/ROOT.ML \
+   a6/*.thy
+	@$(USEDIR) HOL a6
diff -r 5656e3151f17 -r 0ccba84113a1 doc-src/Exercises/2003/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/Makefile	Tue Apr 06 16:10:39 2004 +0200
@@ -0,0 +1,48 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV2003
+#
+
+SESSIONS = a1 a2 a3 a5
+
+## targets
+
+default: sessions
+sessions: $(SESSIONS)
+
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML a1/*.thy
+	isatool make
+
+## a2
+
+a2: a2/generated/session.tex
+
+a2/generated/session.tex: a2/ROOT.ML a2/*.thy
+	isatool make
+
+## a3
+
+a3: a3/generated/session.tex
+
+a3/generated/session.tex: a3/ROOT.ML a3/*.thy
+	isatool make
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML a5/*.thy
+	isatool make
+
+## a6
+
+ a6: a6/generated/session.tex
+
+ a6/generated/session.tex: a6/ROOT.ML a6/*.thy
+	isatool make