new_type : string * int -> unit
STRUCTURE
Theory
SYNOPSIS
Declares a new type or type constructor.
DESCRIPTION
A call new_type(t,n) declares a new n-ary type constructor called t in the current theory segment. If n is zero, this is just a new base type.
FAILURE
Never fails, but issues a warning if the name is not a valid type name. It will overwrite an existing type operator with the same name in the current theory.
EXAMPLE
A non-definitional version of ZF set theory might declare a new type set and start using it as follows: 
   - new_theory "ZF";
   <<HOL message: Created theory "ZF">>
   > val it = () : unit

   - new_type ("set", 0);
   > val it = () : unit

   - new_constant ("mem", Type`:set->set->bool`);
   > val it = () : unit

   - new_axiom ("EXT", Term`(!z. mem z x = mem z y) ==> (x = y)`);
   > val it = |- (!z. mem z x = mem z y) ==> (x = y) : thm

SEEALSO
types, new_constant, new_axiom
HOL  Trindemossen-1