diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Advanced.thy --- 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