| changeset 50530 | 6266e44b3396 |
| parent 49985 | 5b4b0e4e5205 |
| child 51557 | 4e4b56b7a3a5 |
| 50529:b2aa899b3f2d | 50530:6266e44b3396 |
|---|---|
1 (* Title: HOL/Tools/refute.ML |
1 (* Title: HOL/Library/refute.ML |
2 Author: Tjark Weber, TU Muenchen |
2 Author: Tjark Weber, TU Muenchen |
3 |
3 |
4 Finite model generation for HOL formulas, using a SAT solver. |
4 Finite model generation for HOL formulas, using a SAT solver. |
5 *) |
5 *) |
6 |
6 |