changeset 346 | 0fea8b7a14a1 |
parent 344 | 83d5bca38bec |
child 357 | 80b56d9b322f |
--- a/ProgTutorial/Parsing.thy Mon Oct 12 17:07:17 2009 +0200 +++ b/ProgTutorial/Parsing.thy Tue Oct 13 22:57:25 2009 +0200 @@ -1,8 +1,17 @@ theory Parsing imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package" -uses "Parsing.ML" begin +(*<*) +setup {* +open_file_with_prelude +"Parsing_Code.thy" +["theory Parsing", + "imports Base \"Package/Simple_Inductive_Package\"", + "begin"] +*} +(*>*) + chapter {* Parsing *} text {*