changeset 557 | 77ea2de0ca62 |
parent 538 | e9fd5eff62c1 |
child 562 | daf404920ab9 |
--- 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)