diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Indicator_Function.thy --- a/src/HOL/Library/Indicator_Function.thy Sun Nov 02 17:16:01 2014 +0100 +++ b/src/HOL/Library/Indicator_Function.thy Sun Nov 02 17:20:45 2014 +0100 @@ -2,7 +2,7 @@ Author: Johannes Hoelzl (TU Muenchen) *) -header {* Indicator Function *} +section {* Indicator Function *} theory Indicator_Function imports Complex_Main