38 val var: T list -> indexname * T list |
38 val var: T list -> indexname * T list |
39 val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
39 val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
40 val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
40 val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
41 val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
41 val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
42 val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
42 val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) |
43 val global_typ_no_norm: theory * T list -> typ * (theory * T list) |
43 val global_typ_raw: theory * T list -> typ * (theory * T list) |
44 val global_typ: theory * T list -> typ * (theory * T list) |
44 val global_typ: theory * T list -> typ * (theory * T list) |
45 val global_term: theory * T list -> term * (theory * T list) |
45 val global_term: theory * T list -> term * (theory * T list) |
46 val global_prop: theory * T list -> term * (theory * T list) |
46 val global_prop: theory * T list -> term * (theory * T list) |
47 val local_typ_no_norm: Proof.context * T list -> typ * (Proof.context * T list) |
47 val local_typ_raw: Proof.context * T list -> typ * (Proof.context * T list) |
48 val local_typ: Proof.context * T list -> typ * (Proof.context * T list) |
48 val local_typ: Proof.context * T list -> typ * (Proof.context * T list) |
49 val local_term: Proof.context * T list -> term * (Proof.context * T list) |
49 val local_term: Proof.context * T list -> term * (Proof.context * T list) |
50 val local_prop: Proof.context * T list -> term * (Proof.context * T list) |
50 val local_prop: Proof.context * T list -> term * (Proof.context * T list) |
51 val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list) |
51 val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list) |
52 val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list) |
52 val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list) |
169 |
169 |
170 (* terms and types *) |
170 (* terms and types *) |
171 |
171 |
172 fun gen_item read = Scan.depend (fn st => name >> (pair st o read st)); |
172 fun gen_item read = Scan.depend (fn st => name >> (pair st o read st)); |
173 |
173 |
174 val global_typ_no_norm = gen_item (ProofContext.read_typ_no_norm o ProofContext.init); |
174 val global_typ_raw = gen_item (ProofContext.read_typ_raw o ProofContext.init); |
175 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init); |
175 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init); |
176 val global_term = gen_item (ProofContext.read_term o ProofContext.init); |
176 val global_term = gen_item (ProofContext.read_term o ProofContext.init); |
177 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init); |
177 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init); |
178 |
178 |
179 val local_typ_no_norm = gen_item ProofContext.read_typ_no_norm; |
179 val local_typ_raw = gen_item ProofContext.read_typ_raw; |
180 val local_typ = gen_item ProofContext.read_typ; |
180 val local_typ = gen_item ProofContext.read_typ; |
181 val local_term = gen_item ProofContext.read_term; |
181 val local_term = gen_item ProofContext.read_term; |
182 val local_prop = gen_item ProofContext.read_prop; |
182 val local_prop = gen_item ProofContext.read_prop; |
183 |
183 |
184 |
184 |