diff -r ed797395fab6 -r 007922777ff1 ProgTutorial/Parsing.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ProgTutorial/Parsing.ML Mon Aug 17 20:57:32 2009 +0200 @@ -0,0 +1,7 @@ +(* *) + +open_file_prelude +"Parsing_Code.thy" +(cat_lines ["theory Parsing", + "imports Base \"Package/Simple_Inductive_Package\"", + "begin"]) \ No newline at end of file