add lemmas about comparisons of Fract a b with 0 and 1

merged

add lemma diff_Suc_1

Added lemmas for normalizing freshness results involving fresh_star.

Added typing and evaluation relations, together with proofs of preservation and progress (i.e. part 2A of the POPLmark challenge).

merged

Use LocalTheory.full_name instead of Sign.full_name, because the latter does not work properly for locales.

Replaced Logic.unvarify by Variable.import_terms to make declaration of equivariance lemmas work in locales.

nominal_inductive and equivariance now work on local_theory.

Added equivariance lemmas for fresh_star.

NEWS

merged

robustified

make more proofs work whether or not One_nat_def is a simp rule

add simp rules for numerals with 1::nat

fix lemma hypreal_hnorm_def

make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules

move lemma dvd_mod_imp_dvd into class semiring_div

merged

improved treatment of case certificates

repaired order of variable node allocation

explicitly import Fact

change imports to move Fact.thy outside Plain

add lemmas poly_{div,mod}_minus_{left,right}

merged

declare scaleR distrib rules [algebra_simps]; cleaned up

clean up instantiations

merged

simplify some proofs

remove duplicate instance declaration

stripped classrels_of, instances_of

use canonical subalgebra projection

experimental switch to new well-sorting algorithm

handle NONE case in arity function properly

clarified status of variables in evaluation terms; tuned header

subalgebra: drop arities if desired

merged

more liberality needed

merged

added lemmas

merged

simplified evaluation

merged

added dvd_div_mult

merged

first attempt to solve evaluation bootstrap problem

formal dependency on newly emerging algorithm

merged