tidied; weakened the (impossible) premises of setsum_UN_disjoint

new module for heaps

now uses the heap data structure for BEST_FIRST

new file heap.ML

changed the Schubert Steamroller proof

another brick in the wall

changed a step for the improved rules for setsum

deleted a step made redundant by the improved rules for setsum

replaced the useless [p]subset_insertD by [p]subset_insert_iff

now setsum f A = 0 unless A is finite

now setsum f A = 0 unless A is finite; proved setsum_cong

real simprocs

fixed for removal of subset_empty

this proof needs more detail

uncommented the last 2 examples; tidied

new lemma real_minus_diff_eq

fixed the installation of linear arithmetic for the reals

some missing simprules for integer linear arithmetic

tidied for new card_seteq

subset_empty is no longer a simprule

renamed psubset_card -> psubset_card_mono

Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT

inserted some "addsimps [subset_empty]"; also tidied (a lot)

tracing flag for arith_tac

Now also proves monotonicity when in quick_and_dirty mode.

tidied

full_rename_numerals -> rename_numerals; tidied

a big tidy-up

installing the cancel_numerals and combine_numerals simprocs

tuned tappl syntax;

theorems [cases type: bool] = case_split;

full_rename_numerals -> rename_numerals; tidied

tidied a proof using new lemmas for signs of products

new lemmas for signs of products

new default simprules for m*n = 0

tuned;

rename @case to _case_syntax (improves on low-level errors);

updated;

qed_spec_mp: strip_shyps_warning;

* browser info session directories are now self-contained (may be put on WWW server seperately);

prf_open/close;

replacing 0hr by (0::hypreal)

minor tuning for pdf documents

tidied

provide TAGS file for Isabelle sources;

string syntax: allow \\ \" \\n only;

update_thy_only: setmp Thm.trace_simp false;

renamed mktags to maketags;

generate TAGS file for Isabelle sources;

Removed cp / mkdir commands for graph browser files.

Exported system_command.

Removed codebase attribute from applet_pages.

Reorganized graph stuff.

First round of changes, towards installation of simprocs * replacing 0r by (0::real0 * better rewriting, especially pulling out signs in (-x)*y = - (x*y), etc.

Real/simproc.ML now removed

tidied

pair split: proper names of params;

added rule_params;

session.tex: nsert blank lines in order to guarantee new paragraphs for each file (otherwise TeX would easily choke on large input);

opt_mixfix', opt_infix';

do not setmp Library.timing;

removed explicit terminator (";");

removed method;

improved terminator msg;

block commands: marginal comment;

fixed Thm.eq_thm: use Sign.joinable;

'next', '{', '}': comment;

removed brace aliases;

added HOL/Prolog

The Allocator Implementation (not yet working)

lots of new results about sublist, bag_of

new theorem increasing_constant

new constant bag_of

added eta_contract_eq, also to simpset

added rtranclD, tranclD, irrefl_trancl_rD

new theorems Always_Constrains_weaken and Always_Compl_Un_eq

added split_eta_SetCompr2 (also to simpset), generalized SetCompr_Sigma_eq

new parent MultisetOrder and new results about multiset unions

added map_of_mapk_SomeI and weak_map_of_SomeI

Many new theorems about multisets and their ordering, including basic laws like {#} <= M. Renamed union_comm to union_commute. Introduced the collection operator {# x:M. P x #}.

*** empty log message ***

added HOL/Prolog

simplified the proof of nth_upt

Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added.

switched to Isar proofs

Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to the current context is now done automatically);

Toplevel.no_timing;

transfer now automatic;

removed 'transfer' att (is now automatic);

get_thm(s): automatic transfer;

tuned tactic emulation;

removed 'transfer' att;

moved some theorems to Finite.ML

added new proofs and simplified an old one

new theorems (some from Multiset)

the is now defined using primrec, avoiding explicit use of arbitrary.

cleaned up;

global timing flag;

fixed comment;

renamed trace/stat_norm_ast to trace/stat_ast;

renamed Syntax.trace_norm_ast to Syntax.trace_ast; removed Syntax.stat_norm_ast;

proof_timing replaced by global timing;

* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global timing flag supersedes proof_timing and Toplevel.trace;

Collect_neg_eq;

\newcommand{\indexisarcase};

case 'antecedent';

write major keywords;

sublist and some lemmas about it

a more robust proof

fixed the dependences

tidied

restored some of the lessThans

addss -> force_tac

named the primrec clauses of upt

renamed upt_Suc, since that name is needed for its primrec rule

new setsum results

tuned case_tac;

updated acknowledgements

fixed the documentation of goalw_cterm and prove_goalw_cterm

res_inst_tac, etc., no longer print the "dest_state" message when the selected subgoal does not exist