| changeset 56455 | 1ff66e72628b |
| parent 56454 | e9e82384e5a1 |
| child 56456 | 39281b3e4fac |
--- a/src/HOL/BNF_Examples/Compat.thy Tue Apr 08 18:06:21 2014 +0200 +++ b/src/HOL/BNF_Examples/Compat.thy Tue Apr 08 18:16:47 2014 +0200 @@ -52,14 +52,12 @@ | "f_mylist (MyCons _ xs) = Suc (f_mylist xs)" datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar -(* FIXME datatype_compat bar' foo' fun f_foo and f_bar where "f_foo FooNil = 0" | "f_foo (FooCons bar foo) = Suc (f_foo foo) + f_bar bar" | "f_bar Bar = Suc 0" -*) locale opt begin