src/HOL/Tools/simpdata.ML
changeset 37744 3daaf23b9ab4
parent 36603 d5d6111761a6
child 38558 32ad17fe2b9c
equal deleted inserted replaced
37743:0a3fa8fbcdc5 37744:3daaf23b9ab4
     1 (*  Title:      HOL/simpdata.ML
     1 (*  Title:      HOL/Tools/simpdata.ML
     2     Author:     Tobias Nipkow
     2     Author:     Tobias Nipkow
     3     Copyright   1991  University of Cambridge
     3     Copyright   1991  University of Cambridge
     4 
     4 
     5 Instantiation of the generic simplifier for HOL.
     5 Instantiation of the generic simplifier for HOL.
     6 *)
     6 *)