src/HOL/Import/shuffler.ML
changeset 14620 1be590fd2422
parent 14518 c3019a66180f
child 14818 ad83019a66a4
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4 -(*  Title:      Provers/shuffler.ML
     1.5 +(*  Title:      HOL/Import/shuffler.ML
     1.6      ID:         $Id$
     1.7      Author:     Sebastian Skalberg, TU Muenchen
     1.8 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10  Package for proving two terms equal by normalizing (hence the
    1.11  "shuffler" name).  Uses the simplifier for the normalization.