| changeset 60770 | 240563fbf41d |
| parent 41779 | a68f503805ed |
| child 65449 | c82e63b11b8b |
--- a/src/ZF/Coind/Language.thy Thu Jul 23 14:20:51 2015 +0200 +++ b/src/ZF/Coind/Language.thy Thu Jul 23 14:25:05 2015 +0200 @@ -6,7 +6,7 @@ theory Language imports Main begin -text{*these really can't be definitions without losing the abstraction*} +text\<open>these really can't be definitions without losing the abstraction\<close> axiomatization Const :: i and (* Abstract type of constants *)