src/HOL/simpdata.ML
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;