| changeset 50530 | 6266e44b3396 | 
| parent 49985 | 5b4b0e4e5205 | 
| child 51557 | 4e4b56b7a3a5 | 
--- a/src/HOL/Library/refute.ML Fri Dec 14 16:24:12 2012 +0100 +++ b/src/HOL/Library/refute.ML Fri Dec 14 16:33:22 2012 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/refute.ML +(* Title: HOL/Library/refute.ML Author: Tjark Weber, TU Muenchen Finite model generation for HOL formulas, using a SAT solver.