ProgTutorial/General.thy
changeset 346 0fea8b7a14a1
parent 345 4c54ef4dc84d
child 347 01e71cddf6a3
--- a/ProgTutorial/General.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/General.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -2,7 +2,16 @@
 imports Base FirstSteps
 begin
 
-chapter {* Let's Talk About the Good, the Bad and the Ugly *}
+(*<*)
+setup{*
+open_file_with_prelude 
+  "General_Code.thy"
+  ["theory General", "imports Base FirstSteps", "begin"]
+*}
+(*>*)
+
+
+chapter {* Isabelle in More Detail \mbox{or, the Good, the Bad and the Ugly} *}
 
 text {*
   Isabelle is build around a few central ideas. One central idea is the