41 val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
41 val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
42 val global_typ_raw: theory * T list -> typ * (theory * T list) |
42 val global_typ_raw: theory * T list -> typ * (theory * T list) |
43 val global_typ: theory * T list -> typ * (theory * T list) |
43 val global_typ: theory * T list -> typ * (theory * T list) |
44 val global_term: theory * T list -> term * (theory * T list) |
44 val global_term: theory * T list -> term * (theory * T list) |
45 val global_prop: theory * T list -> term * (theory * T list) |
45 val global_prop: theory * T list -> term * (theory * T list) |
46 val local_typ_raw: Proof.context * T list -> typ * (Proof.context * T list) |
46 val local_typ_raw: ProofContext.context * T list -> typ * (ProofContext.context * T list) |
47 val local_typ: Proof.context * T list -> typ * (Proof.context * T list) |
47 val local_typ: ProofContext.context * T list -> typ * (ProofContext.context * T list) |
48 val local_term: Proof.context * T list -> term * (Proof.context * T list) |
48 val local_term: ProofContext.context * T list -> term * (ProofContext.context * T list) |
49 val local_prop: Proof.context * T list -> term * (Proof.context * T list) |
49 val local_prop: ProofContext.context * T list -> term * (ProofContext.context * T list) |
50 val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list) |
50 val bang_facts: ProofContext.context * T list -> thm list * (ProofContext.context * T list) |
51 val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list) |
51 val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list) |
52 -> ((int -> tactic) -> tactic) * ('a * T list) |
52 -> ((int -> tactic) -> tactic) * ('a * T list) |
53 type src |
53 type src |
54 val src: (string * T list) * Position.T -> src |
54 val src: (string * T list) * Position.T -> src |
55 val dest_src: src -> (string * T list) * Position.T |
55 val dest_src: src -> (string * T list) * Position.T |