instance preal :: ordered_cancel_ab_semigroup_add

use new-style class for sq_ord; rename op << to sq_le

take out Class.thy again, because it does not yet compile cleanly

add axclass semiring_char_0 for types where of_nat is injective

changed filter syntax from : to <-

hide filter

tuned list comprehension, changed filter syntax from : to <-

clean up proofs of exp_zero, sin_zero, cos_zero

generalize class constraints on some lemmas

generalize of_nat and related constants to class semiring_1

declare complex_diff as simp rule

New Reflected Presburger added to HOL/ex

Groebner Basis Examples.

print_antiquotations: sort_strings;

tuned document; added Groebner_Examples;

tuned source deps;

simplified/renamed add_numerals;

renamed ex/Eval_Examples.thy;

added ex/Groebner_Examples.thy; renamed ex/Eval_Examples.thy;

tuned document;

Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic

Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers

tuned boostrap

eliminated Code_Generator.thy

tuned integers

tuned;

fixed type int vs. integer;

renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;