--- 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
--- 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
--- 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}