tuned heading
authorhaftmann
Thu, 19 Apr 2012 09:31:36 +0200
changeset 484431e18bbfb40cb
parent 48442 1d9faa9f65f9
child 48444 6244475356ba
tuned heading
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Wed Apr 18 21:47:26 2012 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Apr 19 09:31:36 2012 +0200
     1.3 @@ -579,7 +579,7 @@
     1.4    in (nbe_program, idx_tab) end;
     1.5  
     1.6  
     1.7 -(* dynamic evaluation oracle *)
     1.8 +(* evaluation oracle *)
     1.9  
    1.10  fun mk_equals thy lhs raw_rhs =
    1.11    let