changeset 53609 | 0f472e7063af |
parent 53603 | 59ef06cda7b9 |
child 53610 | dde3cc2804cc |
--- a/src/HOL/Tools/Function/fun_cases.ML Mon Sep 09 00:14:07 2013 +0200 +++ b/src/HOL/Tools/Function/fun_cases.ML Mon Sep 09 00:53:50 2013 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Tools/Function/fun_cases.ML - Author: Manuel Eberl <eberlm@in.tum.de>, TU München + Author: Manuel Eberl, TU Muenchen Provides the fun_cases command for generating specialised elimination rules for function package functions.