added Haftmann-Wenzel:2009;

updated generated files;

isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;

merged

include HOL-Decision_Procs in stats;

back to plain http;

merged

Added postprocessing rules for fresh_star.

Fixed nonexhaustive match problem in decomp, to make it fail more gracefully in case assumptions are not of the form (Trueprop $ ...).

tuned NEWS;

merged

merged

add type annotation

disable floor_minus and ceiling_minus [simp]

merged

merged

Updated the theory syntax. Corrected an error in a command.

merged

generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono

new theory of Archimedean fields

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

name fix

fix spelling

real_inner class instance for vectors

NEWS

merged

Removed subsumed lemmas

remove duplicated lemmas about norm

real_normed_vector instance

fix real_vector, real_algebra instances

merged

generalize lemmas from nat to 'a::wellorder

generalize some lemmas

merged

removed redundant thms

merged

class instances for num1

Removed redundant lemmas

merged

also consider superclasses properly

merged

removed subsumed lemmas

merged

datatype antiquotation: always bracket types with spaces in between

consequent use of term `code equation`

permissive check for pattern discipline in case schemes

maintain order of constructors in datatypes; clarified conventions for type schemes

stripped Id

merged

add theory of products as real vector spaces to Library

add new theory Product_plus.thy to Library

merged

changed message

detailed information on atp-failure via Output.debug

merged

reverted to old wellsorting algorithm

fixed spurious proof failure

consider changes variable names in theorem le_imp_power_dvd

tuned and incremental version of wellsorting algorithm

ignore sorts in bare types

defensive implementation of pretty serialisation of lists and characters

dropped Id

experimental inclusion of new wellsorting algorithm for code equations

merged

merged

merged

fixed selection of premises

cleaned up

declare of_int_number_of_eq [simp]

fix case_names

nicer induction/cases rules for numeral types

number_ring instances for numeral types

declare xor_compl_{left,right} [simp]