using class instance

dvd_def now with object equality

op div/op mod now named without leading op

workaround for definition violating type discipline

moved dvd stuff to theory Divides

re-eliminated thm trichotomy

power is now a class

tuned

clarified module dependencies

div is now a class

reduced verbosity

adjustments for class package

added an intro lemma for freshness of products; set up the simplifier so that it can deal with the compact and long notation for freshness constraints (FIXME: it should also be able to deal with the special case of freshness of atoms)

more robust syntax for definition/abbreviation/notation;

'notation': more robust 'and' list;

updated;

added Isar.goal;

added where_;

add lemmas LIM_zero_iff, LIM_norm_zero_iff

Includes type:sort constraints in its code to collect predicates in axiom clauses.

Now includes only types used to instantiate overloaded constants in arity clauses

added General/basics.ML;

moved some fundamental concepts to General/basics.ML;

Fundamental concepts.

add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);

tuned proofs;

replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;

replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; declared intro/elim rules;

dropping accidental self-imports

corrected polymorphism check