tuned spelling;
authorwenzelm
Thu Oct 30 16:17:56 2014 +0100 (2014-10-30)
changeset 588364037bb00d08e
parent 58835 462ec23aa92f
child 58837 e84d900cd287
tuned spelling;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu Oct 30 15:57:13 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Oct 30 16:17:56 2014 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4   {thm: thm,         (*the rewrite rule*)
     1.5    name: string,     (*name of theorem from which rewrite rule was extracted*)
     1.6    lhs: term,        (*the left-hand side*)
     1.7 -  elhs: cterm,      (*the etac-contracted lhs*)
     1.8 +  elhs: cterm,      (*the eta-contracted lhs*)
     1.9    extra: bool,      (*extra variables outside of elhs*)
    1.10    fo: bool,         (*use first-order matching*)
    1.11    perm: bool};      (*the rewrite rule is permutative*)