Replacing impOfSubs analz_mono by analz_insertI should improve convergence of spy_analz_tac

Renamed set_of_list to set, and relevant theorems too

Replaced Suc(Suc 0) by 2; it improves readability a little

Renamed theorems of the form set_of_list_XXX to set_XXX

Added select1_equality

added append_file;

This file has moved to Distribution/lib/images.

This file has moved to Distribution/lib/html.

Removed references to simplifier.

Modified parse error message.

Startup script for Isabelle theory browser.

Modified graph data directory.

Added some commands for building theory browser.

Added new environment variable ISABELLE_BROWSER_INFO.

Added some code for generating theory browsing data.

Gif images which are copied to $ISABELLE_BROWSER_INFO when theory browsing data is generated.

Index file which is copied to $ISABELLE_BROWSER_INFO when theory browsing data is generated.

added str_of_classrel;

added "Proving ..." msgs;

renamed use_string to use_strings;

removed smlnj-1.07;

prs instead of TextIO.output;

tuned copy_file;

tuned names;

tuned;

ThmDatabase;

added read_file, write_file;

tuned; removed qed_spec_mp;

use ThySyn.add_syntax;

tuned comments;

oops;

eliminated ThySynData and ThySynFun; added ThySyn.add_syntax;

obsolete!

Replaced "init_thy_reader" by "set_parser".

Removed references to "thy_data.ML".

Moved some functions which used to be part of thy_data.ML

Moved functions contained in this file to HOL.ML, datatype.ML, simpdata.ML and cladata.ML.

Replaced "init_thy_reader" by "set_parser".

Removed reference to "thy_data.ML".

The functions in this file have been moved to "cladata.ML" and "simpdata.ML".

Moved functions from file "thy_data.ML".

Replaced "init_thy_reader" by "set_parser".

Replaced "init_thy_reader" by set_parser.

Added some new dependencies for files in subdirectory Thy.

Added function "file_exists".

Removed function file_exists (now included in library.ML)

Moved functions for theory information storage / retrieval from thy_read.ML to thy_info.ML .

This file now contains all functions for generating html and graph data.

Moved several functions: html generation --> browser_info.ML theory information storage / retrieval --> thy_info.ML theorem storage (qed) --> thm_database.ML

Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.

Added some additional "use" commands for new files (browser_info.ML and thy_info.ML)

Source files for Isabelle theory graph browser. Initial revision.

Makefile for GraphBrowser Initial revision

added getenv;

removed smlnj-1.07;

cleaned up; added getenv;

tuned comments;

removed ML-Systems/smlnj-1.07.ML;

SML/NJ 1.07 no longer supported!

cleaned up; added getenv;

Added example mapf which requires a special congruence rule.

Added function `replicate' and lemmas map_cong and set_replicate.

cleaned up; added getenv;

Corrected a comment

Added a take/dropWhile lemma.

Generalized nth_drop (Conny).

Corected bug in def of dropWhile (also present in Haskell lib!)

Had to remove {x.x=a} = a from !simpset in one proof.

Added {x.x=a} = a to !simpset.

removed split_paired_Ex; fixed proc args;

new simproc

*** empty log message ***

load simplifier.ML (again);

added prems argument to simplification procedures;

remove references to simplifier.ML;

improved rewrite_thm / rewrite_goals to handle conditional eqns;

Added a few lemmas.

Deleted comment.

Replaced clumsy rewriting by the new function simplify on thms.

List.ML: added lemmas by Stefan Merz. simpodata.ML: removed rules about ? now subsumed by simplification proc.

set_of_list -> set

Simplified a few proofs because of improved simplification.

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 & ...

added simplification meta rules;

standard congs;

Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.

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).

Uses new version of Datatype.occs_in_prems

auto update

Removal of tactical STATE

fixed polymorphic val;

tuned congs: standard;

improved simp tracing;

added simplification meta rules;

tmp fix to accomodate rep_ss changes;

added rewrite_thm;

tuned apsome;

added error_msg;

tuned error / warning;

added print_ss; improved merge;

added dest_mss, merge_mss; fixed matching of simproc lhss;

tuned title;

added dest and merge operations;

added pretty_cterm;

improved print_cs;

Cosmetic changes: margins, indentation, ...

Now possibility_tac is an explicit function, in order to delay the evaluation of \!simpset

Cosmetic changes: margins, indentation, ...

Now possibility_tac and basic_possibility_tac are explicit functions, in order to delay the evaluation of \!simpset

Deleted the superfluous assumption A ~= B, which must hold anyway by induction

Fixed the spelling of AUTH_NAMES--it could not have worked before\!

Option is a synonym for General because MLWorks does not yet provide Option as a separate structure

Removal of the tactical STATE

Removal of the tactical STATE

tuned error propagation msg;

defs may now be conditional; improved output of warnings / errors;

renamed |-> <-| <-> to Parse/PrintRule;

tuned warning;

tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;

considered removal of print_goals_ref;