changeset 53651 | ee90c67502c9 |
parent 53207 | 9745b7d4cc79 |
child 53951 | 03b74ef6d7c6 |
--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 11:54:57 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 15:30:17 2013 +0200 @@ -16,7 +16,7 @@ (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state val can_generate_code_cert: thm -> bool -end; +end structure Lifting_Def: LIFTING_DEF = struct @@ -583,4 +583,4 @@ (liftdef_parser >> lift_def_cmd_with_err_handling) -end; (* structure *) +end (* structure *)