fix: common constraints; cond_print_calc: Proof.pretty_thm;

Thm.def_name;

replaced IsarCmd.kill_theory by Toplevel.kill; fix: common constraints; removed "*" keyword;

calculation: thm list; filter differ;

removed kill_theory; print_thms: use Proof.pretty_thms;

removed the_fact; added pretty_thms; fix: common constraints; renamed "facts" to "this"; print_state: tuned "Using facts";

fix: common constraints;

added store/bind_thms;

added theorems; improved files;

added theorems; begin_theory: implicit files;

isar: avoid verbose goal responses;

structure Termtab;

smart_store_thms;

PureThy.smart_store_thms;

tidied some proofs

tidied

tidied

new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration for the overloading of <, while .ML file gets proofs about renaming constants

changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <

proper calculation / induction;

tuned;

OF: "_" as argument;

clean: include HOL-Real-ex;

auto: CHANGED;

make it actually RUN the real examples

new directory HOL/Real/ex of real examples

'iff' attribute;

'arith' method;

'_' theorem; back: only latest command;

tuned;

new results for localTo

a new theorem

tuned;

added MutilatedCheckerboard;

added Isar_examples/MutilatedCheckerboard.thy;

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;