FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG

fixed some weak elim rules

implements a classical version of make_elim

uses a supplied version of make_elim for addDs

warns of weak elim rules and ignores them

tidying and unbatchifying

fixed some abuses of addDs and addEs

got rid of weak elim rule

tidied

fixed some weak elim rules

make_elim -> cla_make_elim; tidied

updated and tidied

tidied a monstrous proof

deleted a redundant bind_thm

using the new theorem wf_not_refl; tidied

rev_notE now makes strong elim rules; tidied the file

declaring and using cla_make_elim

new file Provers/make_elim.ML

replaced arities by instance;

OuterLex.name_of: include val;

excursion_result: transform_error;

eq_prop: eta contract;

tuned msg;

tuned;

avoid \< in input;

export proper induction rule;

bind_thm;

corrected specifications and simplified proofs

isar-strip-terminators;

updated;

tuned;

use with_paths;

prefer mp over subst; tuned;

tuned;

Isar theory output.

Theory headers (old and new-style).

Text with antiquotations of inner items (terms, types etc.).

use Library.change;

adapted to improved presentation; no longer mirror items from structure Latex;

adapted to improved presentation;

excursion_result;

added extern_skolem;

moved header stuff to thy_header.ML; moved theory presentation to isar_output.ML; major cleanup;

added semicolon; added arguments; tuned;

added !!!; added is_semicolon; export incr_line, keep_line, scan_blank, scan_string; added source_proper; added make_lexicon; tuned;

use ThyHeader.args; adapted OuterSyntax.markup_command;

rearranged print commands;

exception OUTPUT_FAIL of (string * Position.T) * exn (*note: actually belongs to isar_output.ML*);

removed obsolete "{}";

added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;

added IsarOutput (token-level theory output);

added exhausted: ('a, 'b) source -> ('a, 'a list) source;

added state: 'a * 'b -> 'a * ('a * 'b);

fbrk: 2 if not taken;

export hidden: string -> string;

tuned;

added change: 'a ref -> ('a -> 'a) -> unit;

Added new theory Lambda/Type.

get_inductive now returns None instead of raising an exception.

Added new theory.

Subject reduction and strong normalization of simply-typed lambda terms.

new theorem trans_O_subset

added the AllocImpl example

genPrefix_trans_O: generalizes genPrefix_trans

added the allocator refinement proof

sum_below f n -> setsum f (lessThan n)

bind_thm(s);

removed some finiteness conditions from bag_of/sublist theorems

working proofs of the basic merge and distributor properties

fixed the merge spec (NbT -> Nclients) and added the distributor spec

new thoerem Always_Follows2; renamed Always_Follows -> Always_Follows1

added with_paths;

fixed deps;

fixed deps;

fixed deps;

new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite

new theorem UN_empty; it and Un_empty inserted by AddIffs

generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split

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)