27 val list1: (T list -> 'a * T list) -> T list -> 'a list * T list |
27 val list1: (T list -> 'a * T list) -> T list -> 'a list * T list |
28 val list: (T list -> 'a * T list) -> T list -> 'a list * T list |
28 val list: (T list -> 'a * T list) -> T list -> 'a list * T list |
29 val global_typ: theory * T list -> typ * (theory * T list) |
29 val global_typ: theory * T list -> typ * (theory * T list) |
30 val global_term: theory * T list -> term * (theory * T list) |
30 val global_term: theory * T list -> term * (theory * T list) |
31 val global_prop: theory * T list -> term * (theory * T list) |
31 val global_prop: theory * T list -> term * (theory * T list) |
32 val global_pat: theory * T list -> term * (theory * T list) |
32 val global_term_pat: theory * T list -> term * (theory * T list) |
|
33 val global_prop_pat: theory * T list -> term * (theory * T list) |
33 val local_typ: Proof.context * T list -> typ * (Proof.context * T list) |
34 val local_typ: Proof.context * T list -> typ * (Proof.context * T list) |
34 val local_term: Proof.context * T list -> term * (Proof.context * T list) |
35 val local_term: Proof.context * T list -> term * (Proof.context * T list) |
35 val local_prop: Proof.context * T list -> term * (Proof.context * T list) |
36 val local_prop: Proof.context * T list -> term * (Proof.context * T list) |
36 val local_pat: Proof.context * T list -> term * (Proof.context * T list) |
37 val local_term_pat: Proof.context * T list -> term * (Proof.context * T list) |
|
38 val local_prop_pat: Proof.context * T list -> term * (Proof.context * T list) |
37 type src |
39 type src |
38 val src: (string * T list) * Position.T -> src |
40 val src: (string * T list) * Position.T -> src |
39 val dest_src: src -> (string * T list) * Position.T |
41 val dest_src: src -> (string * T list) * Position.T |
40 val attribs: T list -> src list * T list |
42 val attribs: T list -> src list * T list |
41 val opt_attribs: T list -> src list * T list |
43 val opt_attribs: T list -> src list * T list |
126 fun gen_item read = Scan.depend (fn st => name >> (pair st o read st)); |
128 fun gen_item read = Scan.depend (fn st => name >> (pair st o read st)); |
127 |
129 |
128 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init); |
130 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init); |
129 val global_term = gen_item (ProofContext.read_term o ProofContext.init); |
131 val global_term = gen_item (ProofContext.read_term o ProofContext.init); |
130 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init); |
132 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init); |
131 val global_pat = gen_item (ProofContext.read_pat o ProofContext.init); |
133 val global_term_pat = gen_item (ProofContext.read_term_pat o ProofContext.init); |
|
134 val global_prop_pat = gen_item (ProofContext.read_prop_pat o ProofContext.init); |
132 |
135 |
133 val local_typ = gen_item ProofContext.read_typ; |
136 val local_typ = gen_item ProofContext.read_typ; |
134 val local_term = gen_item ProofContext.read_term; |
137 val local_term = gen_item ProofContext.read_term; |
135 val local_prop = gen_item ProofContext.read_prop; |
138 val local_prop = gen_item ProofContext.read_prop; |
136 val local_pat = gen_item ProofContext.read_pat; |
139 val local_term_pat = gen_item ProofContext.read_term_pat; |
|
140 val local_prop_pat = gen_item ProofContext.read_prop_pat; |
137 |
141 |
138 |
142 |
139 (* args *) |
143 (* args *) |
140 |
144 |
141 val exclude = explode "(){}[],"; |
145 val exclude = explode "(){}[],"; |