| changeset 58881 | b9556a055632 |
| parent 58729 | e8ecc79aee43 |
| child 59002 | 2c8b2fb54b88 |
--- 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