diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Parsing.thy --- 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 {*