| changeset 61343 | 5b5656a63bd6 |
| parent 61076 | bdc1e2f0a86a |
| child 61424 | c3658c18b7bc |
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Tue Oct 06 17:46:07 2015 +0200 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Tue Oct 06 17:47:28 2015 +0200 @@ -1,6 +1,6 @@ (* Authors: Klaus Aehlig, Tobias Nipkow *) -section {* Testing implementation of normalization by evaluation *} +section \<open>Testing implementation of normalization by evaluation\<close> theory Normalization_by_Evaluation imports Complex_Main