bug in counter example finder

conversion of ZF/Integ/{Int,Bin} to Isar scripts

added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier

tidied

deleted redundant material (quasiformula, ...) and rationalized

fixed the typesetting

*** empty log message ***

Added missing rewrite rule and some arith examples

order_less_irrefl: [simp] -> [iff]

*** empty log message ***

converted Hyperreal/Zorn to Isar format and moved to Library

removal of blast.overloaded

updated;

*** empty log message ***

tuned;

fixed a name clash

improved tell_thm_deps;

various new lemmas for Constructible

completion of the consistency proof for AC

thms_containing: allow "_" in specification;

*** empty log message ***

* Pure: disallow duplicate fact bindings within new-style theory files;

disallow duplicate fact bindings for drafts (i.e. within new-style theory files);

tuned;

avoid duplicate fact bindings;

removed IsarTut;

*** empty log message ***

avoid duplicate fact bindings;

check_file: disallow current dir (typically "");

simplified results; added hook;

simplified results;

Thm.proof_of;

check_goal: produce error instead of warning;

added proof_of;

thms/axms_of_proof: proper handling of MinProof;

result dependency output;

dup_elim: improved error reporting;

*** empty log message ***

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?";