equal
deleted
inserted
replaced
40 string * bool * minimize_command * string * (string * locality) list vector |
40 string * bool * minimize_command * string * (string * locality) list vector |
41 * thm * int |
41 * thm * int |
42 type isar_params = |
42 type isar_params = |
43 string Symtab.table * bool * int * Proof.context * int list list |
43 string Symtab.table * bool * int * Proof.context * int list list |
44 type text_result = string * (string * locality) list |
44 type text_result = string * (string * locality) list |
|
45 |
|
46 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
|
47 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
|
48 |
|
49 fun find_first_in_list_vector vec key = |
|
50 Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key |
|
51 | (_, value) => value) NONE vec |
45 |
52 |
46 |
53 |
47 (** SPASS's Flotter hack **) |
54 (** SPASS's Flotter hack **) |
48 |
55 |
49 (* This is a hack required for keeping track of axioms after they have been |
56 (* This is a hack required for keeping track of axioms after they have been |