1997-07-25 wenzelm 1997-07-25 added prems argument to simplification procedures;
1997-07-25 wenzelm 1997-07-25 remove references to simplifier.ML;
1997-07-25 wenzelm 1997-07-25 improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-24 nipkow 1997-07-24 Added a few lemmas.
1997-07-24 nipkow 1997-07-24 Deleted comment.
1997-07-24 nipkow 1997-07-24 Replaced clumsy rewriting by the new function simplify on thms.
1997-07-24 nipkow 1997-07-24 List.ML: added lemmas by Stefan Merz. simpodata.ML: removed rules about ? now subsumed by simplification proc.
1997-07-24 paulson 1997-07-24 set_of_list -> set
1997-07-23 nipkow 1997-07-23 Simplified a few proofs because of improved simplification.
1997-07-23 nipkow 1997-07-23 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to automate reasoning about products. simpdata.ML: added simplification procedure for simplifying existential statements of the form ? x. ... & x = t & ...
1997-07-23 wenzelm 1997-07-23 added simplification meta rules;
1997-07-23 wenzelm 1997-07-23 standard congs;
1997-07-23 paulson 1997-07-23 Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.
1997-07-23 paulson 1997-07-23 Now Datatype.occs_in_prems prints the necessary warning ITSELF. It is also easier to invoke and even works if the induction variable is a parameter (rather than a free variable).
1997-07-23 paulson 1997-07-23 Uses new version of Datatype.occs_in_prems
1997-07-23 paulson 1997-07-23 auto update
1997-07-23 paulson 1997-07-23 Removal of tactical STATE
1997-07-23 wenzelm 1997-07-23 fixed polymorphic val;
1997-07-23 wenzelm 1997-07-23 tuned congs: standard;
1997-07-23 wenzelm 1997-07-23 improved simp tracing;
1997-07-23 wenzelm 1997-07-23 added simplification meta rules;
1997-07-23 wenzelm 1997-07-23 tmp fix to accomodate rep_ss changes;
1997-07-23 wenzelm 1997-07-23 added rewrite_thm;
1997-07-23 wenzelm 1997-07-23 tuned apsome;
1997-07-22 wenzelm 1997-07-22 added error_msg;
1997-07-22 wenzelm 1997-07-22 tuned error / warning;
1997-07-22 wenzelm 1997-07-22 added print_ss; improved merge;
1997-07-22 wenzelm 1997-07-22 added dest_mss, merge_mss; fixed matching of simproc lhss;
1997-07-22 wenzelm 1997-07-22 tuned title;
1997-07-22 wenzelm 1997-07-22 added dest and merge operations;
1997-07-22 wenzelm 1997-07-22 added pretty_cterm;
1997-07-22 wenzelm 1997-07-22 improved print_cs;
1997-07-22 paulson 1997-07-22 Cosmetic changes: margins, indentation, ...
1997-07-22 paulson 1997-07-22 Now possibility_tac is an explicit function, in order to delay the evaluation of \!simpset
1997-07-22 paulson 1997-07-22 Cosmetic changes: margins, indentation, ...
1997-07-22 paulson 1997-07-22 Now possibility_tac and basic_possibility_tac are explicit functions, in order to delay the evaluation of \!simpset
1997-07-22 paulson 1997-07-22 Deleted the superfluous assumption A ~= B, which must hold anyway by induction
1997-07-22 paulson 1997-07-22 Fixed the spelling of AUTH_NAMES--it could not have worked before\!
1997-07-22 paulson 1997-07-22 Option is a synonym for General because MLWorks does not yet provide Option as a separate structure
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-07-18 wenzelm 1997-07-18 tuned error propagation msg;
1997-07-18 wenzelm 1997-07-18 defs may now be conditional; improved output of warnings / errors;
1997-07-18 wenzelm 1997-07-18 renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18 wenzelm 1997-07-18 tuned warning;
1997-07-18 wenzelm 1997-07-18 tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;
1997-07-18 wenzelm 1997-07-18 considered removal of print_goals_ref;
1997-07-18 wenzelm 1997-07-18 defs: allow conditions;
1997-07-18 wenzelm 1997-07-18 tuned warning; improved comments;
1997-07-18 wenzelm 1997-07-18 renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18 wenzelm 1997-07-18 tuned warning;
1997-07-18 wenzelm 1997-07-18 tuned warning; renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18 wenzelm 1997-07-18 improved output channels: normal, warning, error;
1997-07-17 wenzelm 1997-07-17 fixed EqI meta rule;
1997-07-17 mueller 1997-07-17 changes needed for introducing fairness
1997-07-17 mueller 1997-07-17 changes neede for introducing fairness
1997-07-17 mueller 1997-07-17 changes needed for adding fairness
1997-07-16 wenzelm 1997-07-16 fixed merge of internal simprocs;
1997-07-14 paulson 1997-07-14 Changing "lost" from a parameter of protocol definitions to a constant. Advantages: no "lost" argument everywhere; fewer Vars in subgoals; less need for specially instantiated rules Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this theorem was never used, and its original proof was also broken the introduction of the "Notes" constructor.
1997-07-14 paulson 1997-07-14 Fixed delIffs to deal correctly with the D-rule