permuted index;

\PROP;

no_qed; bind_thms;

no_qed;

"this";

tuned;

added bind_thms;

tuned K;

tuned;

from hyp;

added no_qed;

new theorem fun_upd_upd

new SVC url

renamed NatSum to Summation;

tidied;

AddXDs [bspec];

added with_path;

terminal method: always involve finish;

with_path;

renamed improper method 'clarsimp' to 'clarsimp_tac';

added MultisetOrder.thy;

Isar_examples/MultisetOrder.thy;

tuned;

"this";

Wellfoundedness proof for the multiset order (preliminary version).

fix: vars;

removed "*" method combinator;

observe show_types;

bind_thms;

bind_thm "case";

*: no quotes;

Method.insert_tac; Method.multi_resolves; contradiction: made faithful; tuned comments;

Method.insert_tac;

Method.insert_tac; tuned comments;

bind_thm;

added bind_thms, store_thms;

structures Vartab / Termtab (instances of TableFun);

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;