# HG changeset patch
# User nipkow
# Date 976879955 -3600
# Node ID 06f390008ceb649fef155f7973576bbe5177e329
# Parent  0b40c19f09f3665f689229b5b61994887e8b7a43
*** empty log message ***

diff -r 0b40c19f09f3 -r 06f390008ceb doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Thu Dec 14 19:38:37 2000 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Fri Dec 15 12:32:35 2000 +0100
@@ -15,7 +15,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-
+USEDIR = @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL
 
 ## HOL
 
@@ -39,7 +39,7 @@
 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
 
 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr
+	$(USEDIR) Ifexpr
 	@rm -f tutorial.dvi
 
 ## HOL-ToyList
@@ -50,19 +50,19 @@
 	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
 
 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2
+	$(USEDIR) ToyList2
 	@rm -f tutorial.dvi
 
 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList
+	$(USEDIR) ToyList
 	@rm -f tutorial.dvi
 
 ## HOL-CodeGen
 
 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
 
-$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen
+$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy
+	$(USEDIR) CodeGen
 	@rm -f tutorial.dvi
 
 
@@ -73,7 +73,7 @@
 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
   Datatype/Nested.thy Datatype/unfoldnested.thy \
   Datatype/Fundata.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
+	$(USEDIR) Datatype
 	@rm -f tutorial.dvi
 
 
@@ -82,7 +82,7 @@
 HOL-Trie: HOL $(LOG)/HOL-Trie.gz
 
 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
+	$(USEDIR) Trie
 	@rm -f tutorial.dvi
 
 
@@ -93,7 +93,7 @@
 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
   Recdef/simplification.thy Recdef/Induction.thy \
   Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
+	$(USEDIR) Recdef
 	@rm -f tutorial.dvi
 
 
@@ -103,7 +103,7 @@
 
 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \
 	Advanced/Partial.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
+	$(USEDIR) Advanced
 	@rm -f tutorial.dvi
 
 ## HOL-Rules
@@ -130,7 +130,7 @@
 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
 
 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
+	$(USEDIR) CTL
 	@rm -f tutorial.dvi
 
 ## HOL-Inductive
@@ -139,7 +139,7 @@
 
 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
   Inductive/Even.thy Inductive/Star.thy Inductive/AB.thy Inductive/Advanced.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive
+	$(USEDIR) Inductive
 	@rm -f tutorial.dvi
 
 ## HOL-Types
@@ -150,7 +150,7 @@
   Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
+	$(USEDIR) Types
 	@rm -f tutorial.dvi
 
 ## HOL-Misc
@@ -161,7 +161,7 @@
   Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
   Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
   Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
-	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
+	$(USEDIR) Misc
 	@rm -f tutorial.dvi
 
 
diff -r 0b40c19f09f3 -r 06f390008ceb doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu Dec 14 19:38:37 2000 +0100
+++ b/doc-src/TutorialI/todo.tobias	Fri Dec 15 12:32:35 2000 +0100
@@ -78,11 +78,6 @@
 Tacticals: , ? +
 Note: + is used in typedef section!
 
-Mention that simp etc (big step tactics) insist on change?
-
-Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
-does more.)
-
 A list of further useful commands (rules? tricks?)
 prefer, defer, print_simpset (-> print_simps?)
 
@@ -90,11 +85,9 @@
 Where explained? Should go into a separate section as Inductive needs it as
 well.
 
-Where is "simplified" explained? Needed by Inductive/AB.thy
-
 demonstrate x : set xs in Sets. Or Tricks chapter?
 
-Appendix with HOL keywords. Say something about other keywords.
+Appendix with HOL and Isar keywords.
 
 
 Possible exercises
diff -r 0b40c19f09f3 -r 06f390008ceb doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Thu Dec 14 19:38:37 2000 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Fri Dec 15 12:32:35 2000 +0100
@@ -85,8 +85,8 @@
 \input{Rules/rules}
 \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
 \input{Inductive/inductive}
+\input{Types/types}
 \input{Advanced/advanced}
-\input{Types/types}
 \chapter{Theory Presentation}
 \chapter{Case Study: The Needhamd-Schroeder Protocol}
 \chapter{Structured Proofs}