41 val raw_goal: state -> {context: context, facts: thm list, goal: thm} |
41 val raw_goal: state -> {context: context, facts: thm list, goal: thm} |
42 val goal: state -> {context: context, facts: thm list, goal: thm} |
42 val goal: state -> {context: context, facts: thm list, goal: thm} |
43 val simple_goal: state -> {context: context, goal: thm} |
43 val simple_goal: state -> {context: context, goal: thm} |
44 val let_bind: (term list * term) list -> state -> state |
44 val let_bind: (term list * term) list -> state -> state |
45 val let_bind_cmd: (string list * string) list -> state -> state |
45 val let_bind_cmd: (string list * string) list -> state -> state |
|
46 val write: Syntax.mode -> (term * mixfix) list -> state -> state |
|
47 val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state |
46 val fix: (binding * typ option * mixfix) list -> state -> state |
48 val fix: (binding * typ option * mixfix) list -> state -> state |
47 val fix_cmd: (binding * string option * mixfix) list -> state -> state |
49 val fix_cmd: (binding * string option * mixfix) list -> state -> state |
48 val assm: Assumption.export -> |
50 val assm: Assumption.export -> |
49 (Thm.binding * (term * term list) list) list -> state -> state |
51 (Thm.binding * (term * term list) list) list -> state -> state |
50 val assm_cmd: Assumption.export -> |
52 val assm_cmd: Assumption.export -> |
537 val let_bind_cmd = gen_bind ProofContext.match_bind; |
539 val let_bind_cmd = gen_bind ProofContext.match_bind; |
538 |
540 |
539 end; |
541 end; |
540 |
542 |
541 |
543 |
|
544 (* concrete syntax *) |
|
545 |
|
546 local |
|
547 |
|
548 fun gen_write prep_arg mode args = map_context (fn ctxt => |
|
549 ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args)); |
|
550 |
|
551 in |
|
552 |
|
553 val write = gen_write (K I); |
|
554 |
|
555 val write_cmd = |
|
556 gen_write (fn ctxt => fn (c, mx) => |
|
557 (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx)); |
|
558 |
|
559 end; |
|
560 |
|
561 |
542 (* fix *) |
562 (* fix *) |
543 |
563 |
544 local |
564 local |
545 |
565 |
546 fun gen_fix prep_vars args = |
566 fun gen_fix prep_vars args = |