changeset 61799 | 4cf66f21b764 |
parent 58874 | 7172c7ffb047 |
child 64593 | 50c715579715 |
--- a/src/HOL/Word/Misc_Numeric.thy Mon Dec 07 10:23:50 2015 +0100 +++ b/src/HOL/Word/Misc_Numeric.thy Mon Dec 07 10:38:04 2015 +0100 @@ -2,7 +2,7 @@ Author: Jeremy Dawson, NICTA *) -section {* Useful Numerical Lemmas *} +section \<open>Useful Numerical Lemmas\<close> theory Misc_Numeric imports Main