ProgTutorial/Advanced.thy
changeset 401 36d61044f9bf
parent 400 7675427e311f
child 408 ef048892d0f0
--- 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