| changeset 21045 | 66d6d1b0ddfa |
| parent 20973 | 0b8e436ed071 |
--- a/src/HOL/simpdata.ML Mon Oct 16 14:07:20 2006 +0200 +++ b/src/HOL/simpdata.ML Mon Oct 16 14:07:21 2006 +0200 @@ -202,7 +202,7 @@ end; (*local*) -(* Simproc for Let *) +(* simproc for Let *) val use_let_simproc = ref true; @@ -261,9 +261,9 @@ end; (*local*) -(* A general refutation procedure *) +(* generic refutation procedure *) -(* Parameters: +(* parameters: test: term -> bool tests if a term is at all relevant to the refutation proof;