Three new facts about Image

Replaced \\1 by $1 as Perl itself asked me to...

Fixed the description of recdef

tuned msgs;

improved tracing of rewrite rule application;

removed dead messy code;

added read_var;

tuned;

Updated MOD reference

added symbols syntax;

reorganized into individual theories;

tuned;

make images;

tuned URL;

polyml-3.1;

obsolete;

added thms wrt weakening and strengthening in Abstraction;

New Jersey inactive;

HOL/record;

error with instantiantion of sub-records removed

added record.ML;

tuned;

added unit and prod stuff;

fixed Id;

smlnj-110 factory default;

added of_sort;

added base_path;

added simulations files to IOA;

added forward simulation correectness;

Simplification: sel make and update make

added abstraction files;

added further IOA liles;

updated to Isabelle98;

tuned;

added files containing temproal logic and abstraction;

Delsimprocs nat_cancel;

tuned;

Tidying, mostly to do with handling a more specific version of Fake_parts_insert

tuned;

tuned;

fixed author;

Simplified proofs by omitting PA = {|XA, ...|} from RA2

trivial tidy

tuned;

automatic index.html patch;

tuned;

tuned ISABELLE_TMP_PREFIX;

thm_ord;

eliminated make_ord;

ISABELLE_TMP_PREFIX: $LOGNAME

several minor updates;

tuned;

index.html for Isabelle Distribution Area;

updated to Isabelle98;

tuned;

fixed thm_less;

Expressed most Oops rules using Notes instead of Says, and other tidying

added split_paired_Ex to the implicit simpset

added select_equality to the implicit claset

added select_equality to the implicit claset added split_paired_Ex, split_part, and Eps_split_eq to the implicit simpset removed split_select renamed Collect_Prod to Collect_split

added newline at end of file

*** empty log message ***

streamlined specification of included theories

corrected Title

removed obsolete comment

added Univalent

removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses

added update_same, update_other, update_triv, and map_of_SomeD

replaced fn _ => by K

*** empty log message ***

New rule: image_subset

Restored the ciphertext in OR4 in order to make the spec closer to that in OtwayRees.thy

Tidied by adding more default simprules

adapted to new split order;

adapted to new sort function;

improved targets; fixed dependencies on parent logics;

tuned;

added -u option (again);

Now calls Blast_tac more often

obsolete;

feeder;

Changed required by new blast_tac (the one that squashes flex-flex pairs)

Blast_tac now squashes flex-flex pairs immediately

New theorem image_subsetI

Making proofs faster, especially using keysFor_parts_insert

do require perl;

Auto_tac now has type tactic, not unit->tactic

Declared startTiming and endTiming

use feeder to pipe into ML; cleaned up;

removed -i option;

nth -> !

nth -> !

feed isabelle session;

commented out symboloutput.pl;

added feeder.pl;

pretty_name_space;

removed declared; improved dest;

removed distinct_fst_string;

improved error handling;

fixed execute;

made MLWorks happy;

stderr to $LOG;

Symtab.empty;

improved internal representation;

renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend; renamed Symtan.DUPLICATE to Symtab.DUP;

renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend;

renamed Symtab.null to Symtab.empty;

added >> : (theory -> theory) -> unit;

tuned;

replaced symtab.ML by table.ML;

renamed (is_)null to (is_)empty; renamed DUPLICATE to DUP; renamed extend_new to extend;

Generic tables (lacking delete operation). Implemented as 2-3 trees.

tuned;

export range_type;

improved comment;

More restrictive patterns to prevent changing comments

New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

Tidied using rev_iffD1

Now Blast_tac works properly

Tidied. Also better proof using new blast_tac