* 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);
(*
Degree of polynomials
$Id$
written by Clemens Ballarin, started 22. 1. 1997
*)
Degree = PolyRing +
consts
deg :: ('a::ringS) up => nat
defs
deg_def "deg p == LEAST n. bound n (Rep_UP p)"
end