new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
(* Title: LCF/ex/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Some examples from Lawrence Paulson's book Logic and Computation.
*)
time_use_thy "Ex1";
time_use_thy "Ex2";
time_use_thy "Ex3";
time_use_thy "Ex4";