avoid duplicate fact bindings;

* Isar: preview of problems to finish 'show' now produce an error

conversion of ZF/IntDiv to Isar script

conversion of ZF/IntDiv to Isar script

*** empty log message ***

*** empty log message ***

Added div+mod cancelling simproc

for cancelling div + mod.

updated to use locales (still some rough edges);

tweaked

tweaks

tweaks and new lemmas

new proof needed now

proof can be shortened now

new lemmas

Frederic Blanqui's new "guard" examples

tidying of Isar scripts

Various tweaks of the presentation

Relativized right up to L satisfies V=L!

Tidying up

Relativization and absoluteness for DPow!!

Finished absoluteness of "satisfies"!!

arith_tac should not produce counter example

*** empty log message ***

Counter example generation mods.

Added counter example generation.

*** empty log message ***

In ZF/Constructible, moved many results from Satisfies_absolute, etc., to the new theory Internalize.thy

more robust printing of numerals;

new file Constructible/Satisfies_absolute.thy

Lots of new results concerning recursive datatypes, towards absoluteness of "satisfies"

*** empty log message ***

*** empty log message ***

Added Mi and Max on sets, hid Min and Pls on numerals.

*** empty log message ***

transform_error: pass through Interrupt;

tuned;

exception SIMPROC_FAIL: solid error reporting of simprocs;

tuned prove_conv (error reporting done within meta_simplifier.ML);

adhoc_freeze_vars;

proper instantiation of mk_left_commute;

converted;

tuned deps;

use Tactic.prove instead of prove_goalw_cterm in internal proofs!

Tactic.prove, Tactic.prove_standard;

* Pure: improved error reporting of simprocs; tuned;

tuned;

mk_left_commute: proper instantiation avoids expensive unification;

tuned;

Simplifier.simproc(_i);

Added time example at the end.

section on "Rule declarations and methods";

Removed (now unneeded) declaration of realizer for induction on datatype b.

Removed (now unneeded) declarations of realizers for induction on lists and letters.

Added file Tools/datatype_realizer.ML

Removed (now unneeded) declaration of realizers for induction on natural numbers.

Module for defining realizers for induction and case analysis theorems for datatypes.

Added calls to add_dt_realizers.

Exported function make_tnames.

Fixed two bugs

* Provers: Simplifier.simproc(_i) now provide sane interface for setting up simprocs;

sane interface for simprocs;

fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);

predefined locales "var" and "struct" (useful for sharing parameters);

* Pure: predefined locales "var" and "struct" are useful for sharing parameters (as in CASL, for example); just specify something like ``var x + var y + struct M'' as import;

protect simplifier operation against spurious exceptions from simprocs;

tuned; subsection on simple meta-theory of structures;

special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);

Removed theory NatDef.

Replaced nat_ind_tac by induct_tac.

Removed proof of Suc_le_D (already proved in Nat.thy).

Removed reference to theory NatDef.

Removed reference to simpset of NatDef.thy

Legacy ML bindings.

- Converted to new theory format - Moved NatDef stuff to theory Nat

Moved NatDef stuff to theory Nat.

updated;

added Isabelle LNCSes;

fixed long statement: P.opt_thm_name;

fixed railroads;

typedef: "open" option;

declare projected "axioms" as "elim?";

better satisfies rules for is_recfun A satisfies rule for is_wfrec!

some progress towards "satisfies"

*** empty log message ***

added mk_left_commute to HOL.thy and used it "everywhere"

separate "axioms" proofs: more flexible for locale reasoning

tweaks involving Separation

new theorem eq_commute

better sats rules for higher-order operators

removal of twos_compl.ML, which is not really needed

- changed date format for proper lexicographical ordering - send tail of log in email

changed date format for proper lexicographical ordering

tuned messages;

tuned;

eliminate open locales and special ML code;

tuned document;

make SML/NJ happy;

support for split assumptions in cases (hyps vs. prems);

tuned;

More lemmas, working towards relativization of "satisfies"

Added the assumption nth_replacement to locale M_datatypes. Moved up its proof to make it available for the instantiation of that locale.

simplified locale predicates;

removed unused locale_facts(_i); simplified locale predicates: only one level for zero imports; tuned;

tuned;

tweaks, aiming towards relativization of "satisfies"

Tuned type constraint of function merge_rules to make smlnj happy.

AC18: meta-level predicate via locale;

tuned view;

removed attribute "norm_hhf";

adapted fact names;

predicate defs via locales;

locales: predicate defs;

* Pure: locale specifications now produce predicate definitions;

Relativization and Separation for the function "nth"

Added "nocite" to avoid BibTeX error when proofs are switched off.

Added program extraction keywords.

Document for program extraction in HOL.

Examples for program extraction in HOL.

Rules for rewriting HOL proofs.

Added theory for setting up program extraction.

Added program extraction module.

*** empty log message ***

accomodate cumulative locale predicates;

support locale ``views'' (for cumulative predicates);

Towards relativization and absoluteness of formula_rec

Absoluteness of the function "nth"

A couple of new theorems for Constructible