diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Wed May 28 12:41:09 2014 +0100 +++ b/ProgTutorial/Base.thy Tue Jul 08 11:34:10 2014 +0100 @@ -1,10 +1,6 @@ theory Base imports Main "~~/src/HOL/Library/LaTeXsugar" -(*keywords "ML" "setup" "local_setup" :: thy_decl and - "ML_prf" :: prf_decl and - "ML_val" :: diag -*) begin notation (latex output)