The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;

tuned;

thm "_" = asm_rl;

tidied

use of bij, new theorems, etc.

the bij predicate forced renaming of a variable bij

tidied, allowing pattern-matching in defs of prat_add and prat_mult

tidied, allowing pattern-matching in defs of zadd and zmult

the bij predicate (at last)

better timing information;

oops;

*** empty log message ***

tuned;

iff_attrib_setup;

improved back, help;

print_help;

back: recur flag;

a bit further with property (1)

changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE

new destruction rules

new laws; changed "guar" back to "guarantees" (sorry)

changed "guar" back to "guarantees" (sorry)

more Join rules including AC-rules

extra syntax for JN, making it more like UN

a little tidying; also FIXED BAD TYPE in INTER1, UNION1

proper bootstrap of HOL theory and packages;

expand_classes renamed to intro_classes;

proper bootstrap of IFOL/FOL theories and packages;

proper setup of GlobalClaset data;

improved msg;

fixed arity;

expand_classes renamed to intro_classes;

TPHOLs99;

Removed "Adding axioms ..." message.

hide private parts;

another snapshot

arguably clearer definition of the inductive case of leads-to. No proofs had to be changed...

tidied

new guarantees laws; also better natural deduction style for old ones

renamed some theorems; also better natural deduction style for old ones

project constants

many "project" laws

new guarantees laws; also better natural deduction style for old ones

split_paired_Eps and lemmas

new theorem inv_f_eq

%dir;

tuned;

draft release;

Real/Real.thy main entry point;

isar: no_pos flag;

fixed add_sect etc.;

??thesis: include params;

print_mode activated again;

fixed intro_elim_tac;

record_simproc;

tuned;

record_simproc;

Some changes in sections about Sum and Nat.

simplifier flex heads.

Now rewrite rules with flexible heads are allowed.

isatool expandshort;

tuned;

Moved sum_case to theory HOL/Datatype.

tuned;

Corrected two busg in the simplifier.

\indexisarreg;

\VVar;

checkpoint;

tuned; fixed HOL-Real;

real numerals;

added HOL-Real; made relocatable;

echo ML_PLATFORM;

activate example;

delcongs [if_weak_cong];

print_context;

eliminated HOL-AxClasses target;

intro (no +);

mucke -res;

if_svc_enabled;

AxClasses, Isar_examples;

intro/elim: REPEAT1;

new theories RealBin, RealInt, RealPow

* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;

quite a lot of tuning and cleanup;

sysman: Stefan Berghofer;

more;

Mucke, Einhoven;

quite a lot of tuning an cleanup;

sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.

Moved sum_case stuff from Sum to Datatype.

real literals using binary arithmetic

new entriues.

updated

disabled print_mode (tmp);

lookup_theory;

defer_recdef

removed needless comments

removed all unnecessary code

now with abstraction code previously in HOL/Tools/svc_funcs.ML

documented svc_tac

finished theories;

renamed 'some_rule' to 'rule';

tuned;

removed fixnumerals (for the time being);

tuned Goal syntax;

improved messages;

really removed -m option;

removed -m option;

usedir: removed -m option;

Method.modifier; fixed 'only:';

Method.modifier;

assume: multiple args;