changeset 36393 | be73a2b2443b |
parent 36378 | f32c567dbcaa |
child 36476 | a04cf4704668 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Sun Apr 25 11:38:46 2010 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Author: Jia Meng, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen Storing/printing FOL clauses and arity clauses. Typed equality is treated differently.