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

clarified code for building function equation system; explicit check of type discipline

moved evaluation to Code_Generator.thy

added filter_set; adaptions to more strict type discipline for code lemmas

moved transitivity rules to Orderings.thy

added transitivity rules, reworking of min/max lemmas

dropped dependency on sets

reworking of min/max lemmas