| changeset 61076 | bdc1e2f0a86a |
| parent 58889 | 5b7a9633cfa8 |
| child 61343 | 5b5656a63bd6 |
--- a/src/HOL/ex/Eval_Examples.thy Tue Sep 01 17:25:36 2015 +0200 +++ b/src/HOL/ex/Eval_Examples.thy Tue Sep 01 22:32:58 2015 +0200 @@ -43,7 +43,7 @@ text {* a fancy datatype *} datatype ('a, 'b) foo = - Foo "'a\<Colon>order" 'b + Foo "'a::order" 'b | Bla "('a, 'b) bar" | Dummy nat and ('a, 'b) bar =