more refs;

moved method "iprover" to HOL specific part;

removed Ids;

simultaneous use_thys;

replaced low-level 'no_syntax' by 'no_notation'; tuned header; tuned proofs;

moved generic intuitionistic prover to src/Tools/intuitionistic.ML;

tuned message;

* New prover for coherent logic (see src/Tools/coherent.ML).

more CONTRIBUTORS; fixed some dates;

removed Ids;

moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;

some updates on ancient README;

fixrec package uses new-style syntax and local-theory interface

add function taken_names

merged

make list-style polynomial syntax work when show_sorts is on

more CONTRIBUTORS;

turned "read-only refs" typ_level and minimize_applies into constant values;

merged

removed global ref dfg_format

removed local ref const_needs_hBOOL; renamed some const_min_arity parameters to cma

removed local ref const_min_arity

eliminated private clones of List.partition;

observe some Isabelle/ML coding conventions; avoid structure alias FT, which would complicate systematic searches unnecessarily;

eliminated NJ's List.nth;

tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;

tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;

observe basic Isabelle/ML coding conventions;

moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;

added ML-Systems/polyml-experimental.ML; more systematic treatment of bootstrap files;

tuned;

even less default memory for sunbroy2;

merged

merged

Made then_conv and else_conv available as infix operations.

merged

fixed typo

merged

avoid using legacy type inference

use TheoryData to keep track of pattern match combinators

merged

remove unnecessary simp rules

revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)

merged

back to canonical ROOT, to see if memory problems still persist;

trying less default memory for sunbroy2 test

basic setup for chapter "Syntax and type-checking";

merged

standard headers; eliminated non-ASCII chars, which are fragile in the age of unicode;

updated generated files;

uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities; more robust handling of "|" within index;

fixed import of ~~/src/HOL/Decision_Procs/Ferrack;

more explicit indication of old manuals;

merged

\bibliographystyle{abbrv} for newer ref manuals;

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