equal
deleted
inserted
replaced
52 -> context -> context * ((string * thm list) * thm list) |
52 -> context -> context * ((string * thm list) * thm list) |
53 val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list |
53 val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list |
54 -> context -> context * ((string * thm list) * thm list) |
54 -> context -> context * ((string * thm list) * thm list) |
55 val fix: (string * string option) list -> context -> context |
55 val fix: (string * string option) list -> context -> context |
56 val fix_i: (string * typ) list -> context -> context |
56 val fix_i: (string * typ) list -> context -> context |
|
57 val transfer_used_names: context -> context -> context |
57 val setup: (theory -> theory) list |
58 val setup: (theory -> theory) list |
58 end; |
59 end; |
59 |
60 |
60 signature PROOF_CONTEXT_PRIVATE = |
61 signature PROOF_CONTEXT_PRIVATE = |
61 sig |
62 sig |
684 |
685 |
685 val fix = gen_fixs read_skolemT true; |
686 val fix = gen_fixs read_skolemT true; |
686 val fix_i = gen_fixs cert_typ false; |
687 val fix_i = gen_fixs cert_typ false; |
687 |
688 |
688 |
689 |
|
690 (* transfer_used_names *) |
|
691 |
|
692 fun transfer_used_names (Context {asms = (_, (_, names)), defs = (_, _, _, used), ...}) = |
|
693 map_context (fn (thy, data, (asms, (fixes, _)), binds, thms, (types, sorts, maxidx, _)) => |
|
694 (thy, data, (asms, (fixes, names)), binds, thms, (types, sorts, maxidx, used))); |
|
695 |
689 |
696 |
690 (** theory setup **) |
697 (** theory setup **) |
691 |
698 |
692 val setup = [ProofDataData.init]; |
699 val setup = [ProofDataData.init]; |
693 |
700 |