automatic insertion of datatype intr rules into claset

new typechecking solver for the simplifier

tuned;

Fixed a bug in lin.arith.

tuned;

tuned;

isabelle.in.tum.de;

http://isabelle.in.tum.de/dist/;

renamed variables for clarity

changed Minho mirror;

tidied freeness reasoning

freeness reasoning: T.free_iffs

tuned;

removal of the (thm list) argument of mk_cases

tidied; added dest_eq

simplified thanks to the arithmetic prover

updated comments

a simplification by G Bella

structure Graph = Graph;

GraphFun (generic directed graphs); Graph (graphs indexed by strings);

added General/graph.ML: generic direct graphs;

removed empty line (in case of empty begin_state marker) before Level line added printing of subgoals number in Level line

Removed superfluous arith rules from metric_simps

More Arith.

Fixed old bug: selection of constant to be split should depend not just on the name but also on the type.

nat_arith_tac -> arith_tac

More arith refinements.

tuned README;

Pure/General/symbol.ML;

tuned;

deleted the appendices because documentation exists in the HOL and ZF manuals

defined dquotesoff

new manual ZF

the separate FOL and ZF logics manual, with new material on datatypes and inductive definitions

removal of FOL and ZF

minor updates on inductive definitions and datatypes

fixed titles;

tidying of datatype and inductive definitions

files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;

Refined arithmetic.

congruence rules finally use == instead of = and <->

generalized qed_spec_mp code to work for ZF

datatype package improvements

better qed_spec_mp

Simplified interface.

Simplified arithmetic.

'same' method, 'immediate' proof;

tuned msg;

SYNC;

fixed again;

improved asm_finish;

get_tthms witness theorems;

Split argument structure.

Restructured Arithmatic

*** empty log message ***

verbatim

SYNC;

fixed deriv;

eliminated tthm type and Attribute structure;

tuned msg;

tuned signature;

eliminated global/local names;

eliminated tthm type and Attribute structure;

eliminated tthm type and Attribute structure;

eliminated Attribute structure;

signature BASIC_THM; theorem / axiom deriv: added tags; get/put_name_tags; type attribute;

fixed AUTO_PERL;

show_tags; pretty/print_thms;

added rule_attribute: ('a -> thm -> thm) -> 'a attribute; added tag / untag attributes;

Thm of string * tag list;

eliminated Attribute structure;

removed attribute.ML;

configure AUTO_BASH, AUTO_PERL;

Some simplifications.

More arith simplifications

More arith simplifications.

more robust heap file detection;

tuned, updated;

tidying, e.g. from \\tt to \\texttt

Remoaved a few now redundant rewrite rules.

Added simproc.

Refined arith tactic.

removal of FOL, ZF to a separate manual

removal of DO_GOAL

ZF: the natural numbers as a datatype

if-then-else syntax for ZF

if-then-else syntax for ZF

fixed commit spec;

Simplified proof.

induct_tac and exhaust_tac

primrec, induct_tac

*** empty log message ***

Small mods.

1 proof now automatic.

Instantiated lin.arith.

In Main: moved Bin to the left to preserve the solver in its simpset.

Shortened a proof.

*** empty log message ***

Version 1 of linear arithmetic for nat.

Version 1.0 of linear nat arithmetic.

added new arg for print_tac

new inductive, datatype and primrec packages, etc.

revised datatype definition package

revised inductive definition package

new primrec package

moved from ZF to new subdirectory Tools

new theorem update_type

converted to use new primrec section and update operator

converted to use new primrec section

fixed comment

Needs separate theory Primrec_defs due to new inductive defs package

more efficient strip_quotes using "substring"

Basis Library compatible substring oeration

Added a "message" argument to print_tac

comments

deleted "escape" and "trim"; Basis Library can do string escapes if necessary

String added to BasisLibrary

better indentation

fixed comments

replaced obsolete "trim" by "strip_quotes"