src/HOL/Decision_Procs/Approximation.thy

 
 section "Implement floatarith"
 
 subsection "Define syntax and semantics"
 
-datatype_new floatarith
+datatype floatarith
   = Add floatarith floatarith
   | Minus floatarith
   | Mult floatarith floatarith
   | Inverse floatarith
   | Cos floatarith

   case (Var n)
   from this[symmetric] `bounded_by xs vs`[THEN bounded_byE, of n]
   show ?case by (cases "n < length vs", auto)
 qed
 
-datatype_new form = Bound floatarith floatarith floatarith form
+datatype form = Bound floatarith floatarith floatarith form
               | Assign floatarith floatarith form
               | Less floatarith floatarith
               | LessEqual floatarith floatarith
               | AtLeastAtMost floatarith floatarith floatarith