tuned; renamed same_tac to insert_tac; improved assumption; removed Repeat; immediate_proof: assumption;

any_props: improved error; removed "*" method combinator;

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;