src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
changeset 40271 6014e8252e57
parent 39800 17e29ddd538e
child 41457 3bb2f035203f
equal deleted inserted replaced
40269:151fef652324 40271:6014e8252e57
   103 values 10 "{ys. queen_9 ys}"
   103 values 10 "{ys. queen_9 ys}"
   104 
   104 
   105 
   105 
   106 section {* Example symbolic derivation *}
   106 section {* Example symbolic derivation *}
   107 
   107 
   108 hide_const Plus Pow
   108 hide_const Pow
   109 
   109 
   110 datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   110 datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   111   | Minus expr expr | Uminus expr | Pow expr int | Exp expr
   111   | Minus expr expr | Uminus expr | Pow expr int | Exp expr
   112 
   112 
   113 text {*
   113 text {*