read_typ/term: context_of;

tuned;

added context_of;

logtypes: pretend "dummy" is one;

isatool expandshort;

expandshort usage: forward_tac;

strengthened card_seteq

added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD

added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc

added theorems le_maxI1 and le_maxI2, also in claset

added theorem dvd_reduce

*** empty log message ***

added ftac, eatac, datac, fatac

added smp_tac

added;

isabelle-pdfdocs;

close_block: removed ProofContext.transfer_used_names;

removed thms_closure (unused); removed transfer_used_names; fix: do not declare unconstrained vars;

removed thms_closure (unused);

added README;

tuned;

working snapshot

goal_nonempty: Ex goal for new-style version;

replaced ?? by ?;

eliminated Syntax.binding; put_thms: ignore ""; update_binds_env: Envir.norm_term ensures proper type instantiation;

deactivated ProofContext.transfer_used_names; eliminated PureThy.default_name ("" not stored);

removed text vars;

PureThy.have_thmss: "" replaces None;

Library.equal_lists;

removed Syntax.binding;

removed "_BIND" translation;

removed binding;

removed "_BIND" syntax;

eliminated default_name (thms no longer stored for name "");

ProtoPure: fake empty scope;

equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool;

handle Bind!!

updated;

added \indexisarvar;

removed \VVar;

usage: tell OPTIONS;

added welcome;

usage: tell ISABELLE_USEDIR_OPTIONS;

tuned;

usage: tell current OPTIONS value;

updated;

fixed usepackage;

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;

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