2005-05-17 wenzelm 2005-05-17 updated;
2005-05-17 wenzelm 2005-05-17 var_or_skolem: always print question mark for vars stemming from skolems;
2005-05-17 wenzelm 2005-05-17 added read_variable: optional question mark on input; removed obsolete token_assoc; scan_indexname: improved treatment of \<^isub> and \<^isup>; read_var: more robust against bad input; tuned;
2005-05-17 wenzelm 2005-05-17 substantial tuning -- adapted to common conventions;
2005-05-17 wenzelm 2005-05-17 re-init ml_prompts after loop termination;
2005-05-17 wenzelm 2005-05-17 renamed show_var_qmarks to show_question_marks; renamed TermStyle.lookup_style to TermStyle.the_style;
2005-05-17 wenzelm 2005-05-17 Syntax.read_variable;
2005-05-17 wenzelm 2005-05-17 renamed show_var_qmarks to show_question_marks; string_of_vname: improved treatment of \<^isub> and \<^isup>;
2005-05-17 wenzelm 2005-05-17 renamed show_var_qmarks to show_question_marks; var_or_skolem: proper treatment of show_question_marks via Syntax.read_variable;
2005-05-17 wenzelm 2005-05-17 updated;
2005-05-17 wenzelm 2005-05-17 renamed show_var_qmarks to show_question_marks;
2005-05-17 wenzelm 2005-05-17 removed ISAMODE settings;
2005-05-17 wenzelm 2005-05-17 no longer support isa-FOO interface; removed Isamode; tuned;
2005-05-17 wenzelm 2005-05-17 no longer support isa-FOO interface;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-17 wenzelm 2005-05-17 obsolete;
2005-05-17 paulson 2005-05-17 added comment
2005-05-17 paulson 2005-05-17 streamlined proof using new subst method
2005-05-17 wenzelm 2005-05-17 moved credit to CONTRIBUTORS;
2005-05-17 wenzelm 2005-05-17 moved credit to CONTRIBUTORS; tuned;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-17 wenzelm 2005-05-17 export ISABELLE_HOME, do not normalize; tuned;
2005-05-17 wenzelm 2005-05-17 removed THIS_IS_ISABELLE_ADMIN;
2005-05-17 wenzelm 2005-05-17 removed rev_append; tuned presentation of datatype option: removed apsome, export the and if_none;
2005-05-17 wenzelm 2005-05-17 obsolete;
2005-05-17 wenzelm 2005-05-17 added;
2005-05-17 wenzelm 2005-05-17 proper treatment of directory links; tuned;
2005-05-17 kleing 2005-05-17 use Drule.vars_of_terms
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-05-16 kleing 2005-05-16 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-05-16 kleing 2005-05-16 export parser for "-"
2005-05-16 kleing 2005-05-16 line wrap
2005-05-15 berghofe 2005-05-15 Eta-expanded merge function (to make SmlNJ happy).
2005-05-14 haftmann 2005-05-14 added Proof.context to antiquotation
2005-05-13 dixon 2005-05-13 lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
2005-05-13 nipkow 2005-05-13 -(n::nat) is now regarded as atomic
2005-05-13 schirmer 2005-05-13 Bugfix in syntax translation for record type.
2005-05-12 paulson 2005-05-12 theorem names for caching
2005-05-12 paulson 2005-05-12 memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
2005-05-12 paulson 2005-05-12 first-order now ignores "all"
2005-05-12 nipkow 2005-05-12 fixed a few things and added Haftmann as author
2005-05-11 paulson 2005-05-11 documented new subst method
2005-05-11 haftmann 2005-05-11 corrections
2005-05-11 nipkow 2005-05-11 Added thms by Brian Huffmann
2005-05-10 paulson 2005-05-10 new cterm primitives
2005-05-10 paulson 2005-05-10 oops...cannot use subst here
2005-05-10 kleing 2005-05-10 table centering, headline 'other platform'
2005-05-09 paulson 2005-05-09 unfolding of Ex1
2005-05-09 paulson 2005-05-09 choice_const moved to hologic.ML
2005-05-09 paulson 2005-05-09 from simplesubst to new subst
2005-05-09 haftmann 2005-05-09 minor corrections
2005-05-09 kleing 2005-05-09 made file links local, smoothed text over in some places
2005-05-09 kleing 2005-05-09 made file list nicer
2005-05-09 kleing 2005-05-09 moved description (dist area) out of link
2005-05-09 kleing 2005-05-09 made download links local, provide explicit list of files to download
2005-05-09 kleing 2005-05-09 shortened
2005-05-08 wenzelm 2005-05-08 MAILTO: makarius@sketis.net
2005-05-06 dixon 2005-05-06 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
2005-05-06 haftmann 2005-05-06 added notes for mac os
2005-05-06 haftmann 2005-05-06 Added notes for installation on Windows