changeset 61343 | 5b5656a63bd6 |
parent 58889 | 5b7a9633cfa8 |
child 66453 | cc19f7ca2ed6 |
--- a/src/HOL/ex/Code_Binary_Nat_examples.thy Tue Oct 06 17:46:07 2015 +0200 +++ b/src/HOL/ex/Code_Binary_Nat_examples.thy Tue Oct 06 17:47:28 2015 +0200 @@ -2,7 +2,7 @@ Author: Florian Haftmann, TU Muenchen *) -section {* Simple examples for natural numbers implemented in binary representation. *} +section \<open>Simple examples for natural numbers implemented in binary representation.\<close> theory Code_Binary_Nat_examples imports Complex_Main "~~/src/HOL/Library/Code_Binary_Nat"