| changeset 40271 | 6014e8252e57 |
| parent 39800 | 17e29ddd538e |
| child 41457 | 3bb2f035203f |
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Oct 29 16:04:35 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Oct 29 17:25:22 2010 +0200 @@ -105,7 +105,7 @@ section {* Example symbolic derivation *} -hide_const Plus Pow +hide_const Pow datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr | Minus expr expr | Uminus expr | Pow expr int | Exp expr