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

Proving that multisets are partially ordered New infix syntax for element-hood

Proving that multisets are partially ordered New infix syntax for element-hood New theorem size_union

psubsetI is a safe rule

new file Induct/MultisetOrder.thy

fold_commute, fold_nest_Un_Int, setsum_Un and other new results

tuned;

added NatClass;

show_consts no longer requires show_types;

tuned;

tuned;

obsolete;

added notes;

new Isar version;

replaced {{ }} by { };

cite isabelle-axclass;

improved \BG, \EN;

removed is_type_abbr;

removed is_type_abbr; added certify_class, certify_sort, read_sort; adapted to inner syntax of sorts;

adapted to inner syntax of sorts;

replaced {{ }} by { };

added sort_of_term; export sortT;

added read_sort;

*** empty log message ***

new stuff;

\urlstyle{rm};

snapshot of new Isar'ized version;

added lemma.

fixed link

* HOL/ML: even fewer consts are declared as global (see theories Ord, Lfp, Gfp, WF); this only affects ML packages that refer to const names internally; * 'pr' command: no longer prints theory contexts, but only proof states;

print_state: flag for proof only;

hide: check declared;

added disable_pr, enable_pr;

'pr' now prints actual proof states only;

fewer consts declared as global;

'apply' consumes facts;

Proof General -- if present make this the default;

export generic_simp_tac;

changed to cope with the rewriting of #2+n to Suc(Suc n)

new policy to simplify the use of numerals: #0 -> 0 #1 -> 1 #2 + n -> Suc (Suc n) similarly for n + #2

reverted to old proof of dominoes_tile_row, given new treatment of #2+...

Replaced some definitions involving epsilon by more readable primrec definitions.

alist_rec and assoc are now defined using primrec and thus no longer refer to the recursion combinator list_rec, which should be considered internal.

Removed unnecessary primrec equations of hd and last involving arbitrary.

collected three proofs into rename_client_map_tac

added the dummy theory Integ/NatSimprocs.thy

updated

new simprules needed because of new subtraction rewriting

nat_diff_split' now called nat_diff_split

deleted a lot of obsolete arithmetic lemmas

tidied

new simprules for nat_case and nat_rec simplify_meta_eq now maps #0 to 0 and #1 to 1 in its result

tidying, especially to remove zcompare_rls from proofs

a massive tidy-up

NatSimprocs is now a theory, not a file

new theorem one_le_power

tidied

deleted some redundant simprules Added new simprules for subtraction

new dummy theory; prevents strange errors when loading NatSimprocs.ML

improved name of simproc;