changeset 346 | 0fea8b7a14a1 |
parent 339 | c588e8422737 |
child 351 | f118240ab44a |
--- a/ProgTutorial/Tactical.thy Mon Oct 12 17:07:17 2009 +0200 +++ b/ProgTutorial/Tactical.thy Tue Oct 13 22:57:25 2009 +0200 @@ -2,6 +2,14 @@ imports Base FirstSteps begin +(*<*) +setup{* +open_file_with_prelude + "Tactical_Code.thy" + ["theory Tactical", "imports Base FirstSteps", "begin"] +*} +(*>*) + chapter {* Tactical Reasoning\label{chp:tactical} *} text {*