bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
(* Title: ZF/ArithSimp.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
Arithmetic with simplification
*)
theory ArithSimp = Arith
files "arith_data.ML":
end