1998-01-08 paulson 1998-01-08 Expressed most Oops rules using Notes instead of Says, and other tidying
1998-01-08 oheimb 1998-01-08 added split_paired_Ex to the implicit simpset
1998-01-08 oheimb 1998-01-08 added select_equality to the implicit claset
1998-01-08 oheimb 1998-01-08 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
1998-01-08 oheimb 1998-01-08 added newline at end of file
1998-01-08 oheimb 1998-01-08 *** empty log message ***
1998-01-08 oheimb 1998-01-08 streamlined specification of included theories
1998-01-08 oheimb 1998-01-08 corrected Title
1998-01-08 oheimb 1998-01-08 removed obsolete comment
1998-01-08 oheimb 1998-01-08 added Univalent
1998-01-08 oheimb 1998-01-08 removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
1998-01-08 oheimb 1998-01-08 added update_same, update_other, update_triv, and map_of_SomeD
1998-01-08 oheimb 1998-01-08 replaced fn _ => by K
1998-01-08 wenzelm 1998-01-08 *** empty log message ***
1998-01-08 paulson 1998-01-08 New rule: image_subset
1998-01-08 paulson 1998-01-08 Restored the ciphertext in OR4 in order to make the spec closer to that in OtwayRees.thy
1998-01-08 paulson 1998-01-08 Tidied by adding more default simprules
1998-01-07 wenzelm 1998-01-07 adapted to new split order;
1998-01-07 wenzelm 1998-01-07 adapted to new sort function;
1998-01-07 wenzelm 1998-01-07 improved targets; fixed dependencies on parent logics;
1998-01-06 wenzelm 1998-01-06 tuned;
1998-01-05 wenzelm 1998-01-05 added -u option (again);
1998-01-05 paulson 1998-01-05 Now calls Blast_tac more often
1998-01-02 wenzelm 1998-01-02 obsolete;
1998-01-02 wenzelm 1998-01-02 feeder;
1998-01-02 paulson 1998-01-02 Changed required by new blast_tac (the one that squashes flex-flex pairs)
1998-01-02 paulson 1998-01-02 Blast_tac now squashes flex-flex pairs immediately
1998-01-02 paulson 1998-01-02 New theorem image_subsetI
1998-01-02 paulson 1998-01-02 Making proofs faster, especially using keysFor_parts_insert
1998-01-02 wenzelm 1998-01-02 do require perl;
1998-01-02 paulson 1998-01-02 Auto_tac now has type tactic, not unit->tactic
1998-01-02 paulson 1998-01-02 Declared startTiming and endTiming
1997-12-31 wenzelm 1997-12-31 use feeder to pipe into ML; cleaned up;
1997-12-31 wenzelm 1997-12-31 removed -i option;
1997-12-30 nipkow 1997-12-30 nth -> !
1997-12-30 nipkow 1997-12-30 nth -> !
1997-12-29 wenzelm 1997-12-29 feed isabelle session;
1997-12-29 wenzelm 1997-12-29 commented out symboloutput.pl;
1997-12-29 wenzelm 1997-12-29 added feeder.pl;
1997-12-29 wenzelm 1997-12-29 pretty_name_space;
1997-12-29 wenzelm 1997-12-29 removed declared; improved dest;
1997-12-29 wenzelm 1997-12-29 removed distinct_fst_string;
1997-12-28 wenzelm 1997-12-28 improved error handling;
1997-12-28 wenzelm 1997-12-28 fixed execute;
1997-12-28 wenzelm 1997-12-28 made MLWorks happy;
1997-12-28 wenzelm 1997-12-28 stderr to $LOG;
1997-12-28 wenzelm 1997-12-28 Symtab.empty;
1997-12-28 wenzelm 1997-12-28 improved internal representation;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend; renamed Symtan.DUPLICATE to Symtab.DUP;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty;
1997-12-28 wenzelm 1997-12-28 added >> : (theory -> theory) -> unit;
1997-12-28 wenzelm 1997-12-28 tuned;
1997-12-28 wenzelm 1997-12-28 replaced symtab.ML by table.ML;
1997-12-28 wenzelm 1997-12-28 renamed (is_)null to (is_)empty; renamed DUPLICATE to DUP; renamed extend_new to extend;
1997-12-27 wenzelm 1997-12-27 Generic tables (lacking delete operation). Implemented as 2-3 trees.
1997-12-24 wenzelm 1997-12-24 tuned;
1997-12-24 wenzelm 1997-12-24 export range_type;
1997-12-24 wenzelm 1997-12-24 improved comment;
1997-12-24 paulson 1997-12-24 More restrictive patterns to prevent changing comments