--- a/ProgTutorial/Advanced.thy Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Advanced.thy Sun Nov 22 15:27:10 2009 +0100
@@ -6,7 +6,7 @@
setup{*
open_file_with_prelude
"Advanced_Code.thy"
- ["theory General", "imports Base FirstSteps", "begin"]
+ ["theory Advanced", "imports Base FirstSteps", "begin"]
*}
(*>*)
@@ -29,7 +29,7 @@
section {* Theories\label{sec:theories} (TBD) *}
text {*
- As said above, theories are the most basic layer in Isabelle. They contain
+ Theories, as said above, are the most basic layer in Isabelle. They contain
definitions, syntax declarations, axioms, proofs etc. If a definition is
stated, it must be stored in a theory in order to be usable later
on. Similar with proofs: once a proof is finished, the proved theorem needs