equal
deleted
inserted
replaced
447 |
447 |
448 |
448 |
449 (** Isar setup **) |
449 (** Isar setup **) |
450 |
450 |
451 val _ = |
451 val _ = |
452 Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl ( |
452 Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads" |
453 Parse.term_group -- Parse.name >> (fn (raw_bind, target) => |
453 (Parse.term_group -- Parse.name >> (fn (raw_bind, target) => |
454 Toplevel.theory (add_monad target raw_bind)) |
454 Toplevel.theory (add_monad target raw_bind))); |
455 ); |
|
456 |
455 |
457 val setup = |
456 val setup = |
458 Code_Target.add_target |
457 Code_Target.add_target |
459 (target, { serializer = serializer, literals = literals, |
458 (target, { serializer = serializer, literals = literals, |
460 check = { env_var = "ISABELLE_GHC", make_destination = I, |
459 check = { env_var = "ISABELLE_GHC", make_destination = I, |