1.1 --- a/src/HOL/Library/Simps_Case_Conv.thy Fri Sep 06 12:00:58 2013 +0200
1.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy Fri Sep 06 12:05:01 2013 +0200
1.3 @@ -1,5 +1,5 @@
1.4 -(* Title: HOL/Library/Simps_Case_Conv.thy
1.5 - Author: Lars Noschinski
1.6 +(* Title: HOL/Library/Simps_Case_Conv.thy
1.7 + Author: Lars Noschinski
1.8 *)
1.9
1.10 theory Simps_Case_Conv

2.1 --- a/src/HOL/Library/simps_case_conv.ML Fri Sep 06 12:00:58 2013 +0200
2.2 +++ b/src/HOL/Library/simps_case_conv.ML Fri Sep 06 12:05:01 2013 +0200
2.3 @@ -1,10 +1,10 @@
2.4 (* Title: HOL/Library/simps_case_conv.ML
2.5 Author: Lars Noschinski, TU Muenchen
2.6 - Gerwin Klein, NICTA
2.7 + Author: Gerwin Klein, NICTA
2.8
2.9 - Converts function specifications between the representation as
2.10 - a list of equations (with patterns on the lhs) and a single
2.11 - equation (with a nested case expression on the rhs).
2.12 +Convert function specifications between the representation as a list
2.13 +of equations (with patterns on the lhs) and a single equation (with a
2.14 +nested case expression on the rhs).
2.15 *)
2.16
2.17 signature SIMPS_CASE_CONV =