| changeset 41818 | 6d4c3ee8219d |
| parent 37671 | fa53d267dab3 |
| child 46582 | dcc312f22ee8 |
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Feb 22 17:06:14 2011 +0100 @@ -256,7 +256,7 @@ record tstate = time :: nat -types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>" +type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>" primrec timeit :: "'a time com \<Rightarrow> 'a time com" where