* HOL/datatype: induction rule for arbitrarily branching datatypes is
now expressed as a proper nested rule (old-style tactic scripts may
require atomize_strip_tac to cope with non-atomic premises);
* HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
to "split_conv" (old name still available for compatibility);
* HOL: improved concrete syntax for strings (e.g. allows translation
rules with string literals);
(*
Experimental theory: long division of polynomials
$Id$
Author: Clemens Ballarin, started 23 June 1999
*)
LongDiv = PolyHomo +
consts
lcoeff :: "'a::ringS up => 'a"
eucl_size :: 'a::ringS => nat
defs
lcoeff_def "lcoeff p == coeff (deg p) p"
eucl_size_def "eucl_size p == if p = <0> then 0 else deg p+1"
end