equal
deleted
inserted
replaced
1 (* Author: Jia Meng, Cambridge University Computer Laboratory |
1 (* Title: HOL/Tools/res_clause.ML |
2 Copyright 2004 University of Cambridge |
2 Author: Jia Meng, Cambridge University Computer Laboratory |
3 |
3 |
4 Storing/printing FOL clauses and arity clauses. |
4 Storing/printing FOL clauses and arity clauses. Typed equality is |
5 Typed equality is treated differently. |
5 treated differently. |
|
6 |
|
7 FIXME: combine with res_hol_clause! |
6 *) |
8 *) |
7 |
9 |
8 (*FIXME: combine with res_hol_clause!*) |
|
9 signature RES_CLAUSE = |
10 signature RES_CLAUSE = |
10 sig |
11 sig |
11 val schematic_var_prefix: string |
12 val schematic_var_prefix: string |
12 val fixed_var_prefix: string |
13 val fixed_var_prefix: string |
13 val tvar_prefix: string |
14 val tvar_prefix: string |