src/HOL/simpdata.ML
changeset 21045 66d6d1b0ddfa
parent 20973 0b8e436ed071
     1.1 --- a/src/HOL/simpdata.ML	Mon Oct 16 14:07:20 2006 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Oct 16 14:07:21 2006 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4  end; (*local*)
     1.5  
     1.6  
     1.7 -(* Simproc for Let *)
     1.8 +(* simproc for Let *)
     1.9  
    1.10  val use_let_simproc = ref true;
    1.11  
    1.12 @@ -261,9 +261,9 @@
    1.13  
    1.14  end; (*local*)
    1.15  
    1.16 -(* A general refutation procedure *)
    1.17 +(* generic refutation procedure *)
    1.18  
    1.19 -(* Parameters:
    1.20 +(* parameters:
    1.21  
    1.22     test: term -> bool
    1.23     tests if a term is at all relevant to the refutation proof;