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

setsum replaces sum_below

moved mostly to HOL/SetInterval.ML and UNITY/UNITY.ML

sum_below moved here from Arith

improved error msgs, listing variable names

better indentation; declared function "null"

new default rules

deleted sum_below: no need for it with setsum and lessThan

documented permute_prems

better indentation

overloading of 0

added "done" proof;

proper token_translation for latex mode;

some lemmas about plus_ac0

setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.

setsum is now overloaded on plus_ac0

installing plus_ac0 for nat

we must not require SetInterval this early

installing the plus_ac0 axclass

Adding SetInterval, deleting UNITY/LessThan

added parent

facts about lessThan, etc., mostly from UNITY/LessThan

installing the plus_ac0 simprules

rewrote a very long proof (Key_analz_image_Key) because it had stopped working

overloaded 0

tidying for overloaded 0, setsum, etc.

installing plus_ac0 for multisets

replacing "below" by "lessThan"

installing plus_ac0 for int

restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML

tuned;

"done" command;

fixed index;

restored NatSum.thy

now 0 is overloaded

added type constraint ::nat because 0 is now overloaded

IntRingDefs is now redundant

new type class "zero" so that 0 can be overloaded

finally sum_below is overloaded properly

Multisets have a zero: the empty multiset

defining 0::int to be (int 0)

Now that 0 is overloaded, constant "zero" and its type class "zero" are no longer needed. Also IntRingDefs is redundant

added type constraint ::nat because 0 is now overloaded

theory file NatSum.thy no longer needed new files for the Allocator: AllocBase.{thy,ML}

theory file NatSum.thy no longer needed

Sums of geometric series

use of AllocBase

removal of lessThan; use of AllocBase

declared sum_below

new files for the Allocator

eta-expanded to handle value polymorphism

improved warning messages;

SetInterval

Added SetInterval

new Isar version of HOL-AxClasses-Tutorial;

tuned;

* Pure: changed syntax of local blocks from {{ }} to { }; * Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}";

new Isar version;

tidied and made to work with AddSIs [psubsetI]

further tidying

loading the new theory MultisetOrder

multisets are partially ordered