print fixed names as plain strings;

eliminated old numerals;

use generic 1 instead of Numeral1; use improved iff declaration; tuned;

eliminated Numeral0;

build option enables most basic browser info (for proper recording of session);

build option;

tuned;

eliminated old numerals;

pass build mode to process;

removed export_thm;

trace_rules: only non-empty;

removed obsolete "exported" att;

replace_dummy_patterns: lift over bounds;

iff: always rotate prems;

apply(simp add: three_def numerals) (* FIXME !? *);

unset DISPLAY (again);

* Pure: removed obsolete 'exported' attribute; * Pure: dummy pattern "_" in is/let is now automatically ``lifted'' over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");

*** empty log message ***

moved object_logic.ML to Isar/object_logic.ML;

moved locale.ML to Isar/locale.ML;

moved goal related stuff to goals.ML;

Display.current_goals_markers;

tuned;

moved prove_goalw_cterm to goals.ML; cleaned up;

moved local defs to proof.ML (for locales);

improved source arrangement of obtain;

rearrange sources for locales;

Display.print_current_goals_fn;

Display.print_goals;

Display.pretty_thms;

qualified names;

make this module appeat late in Pure; moved print_current_goals to display.ML; added quick_and_dirty_prove_goalw_cterm (from Isar/skip_proof.ML); added thm database functions (from Thy/thm_database.ML);

print_goals stuff is back (from locale.ML);

reorganize sources to accomodate locales;

corollary;

quick_and_dirty_prove_goalw_cterm;

javac -depend;

-D generated;

Added "clean" target.

Fixed problem with batch mode layout, which caused an AWT exception when no X11 connection was available.

initBrowser now has additional noAWT argument.

Constructor no longer takes font as an argument.

Moved font settings from TreeNode to TreeBrowser.

Moved font settings from Vertex to GraphView.

deleted the redundant first argument of adjust(a,b)

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1, binary numerals in literal arithmetic.

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

keep DISPLAY;

updated;

renamed to Typedefs.thy to avoid conflict with main HOL version;

* proper spacing of consecutive markup elements, especially text blocks after section headings;

\newif\ifisamarkup controls spacing of isabeginpar;

improved spacing;

maintain Latex.flag_markup;

flag_markup;

Types/document/Typedefs;

renamed Typedef.thy to Typedefs.thy (former already present in main HOL);

got rid of separate root.tex;

graceful interpretation of -i/-d/-D options; verbose: additional messages/warnings; include document graph;

include document graph;

document graph option;

conditional: bool -> (unit -> unit) -> unit; std_error: string -> unit;

added TextIO.stdErr;

include document graph; tuned;

document graphs for several sessions;

tuned;

calculational rules moved from FOL to IFOL;

option -g for document graph; removed all presumptions about -d/-D (handled by isabelle process);

option -q also excludes -v true in generated stuff; tuned message;

dvips -q;

removed -v option (handled by isabelle process);

-o pdf: produce *both* eps and pdf; tuned;

* greatly simplified document preparation setup, including more graceful interpretation of isatool usedir -i/-d/-D options, and more instructive isatool mkdir; users should basically be able to get started with "isatool mkdir Test && isatool make"; * theory dependency graph may now be incorporated into documents; isatool usedir -g true will produce session_graph.eps/.pdf for use with \includegraphics of LaTeX;

got rid of ML proof scripts;

induct_method.ML -- proof by cases and induction on sets and types (Isar);

latex output: bold lambda;

got rid of ML proof scripts for Product_Type;

got rid of Provers/split_paired_all.ML;

improved default dependencies;

revert to proper version (!);

GPLed;

tuned;

use abstract product type instead of datatype;

moved atomize stuff to theory HOL;

legacy interfaces for axclass instantiation;

added map_base;

sane internal interfaces for instance;

sane internal interface for add_typedef(_i);

proper setup for abstract product types;

moved InductMethod.setup to theory HOL;

setup generic cases and induction (from Inductive.thy);

guillemot syntax;

improved internal interface of typedef;

abstract product types;

proper proof of split_paired_all (presently unused);

tuned comments;

added mk_UNIV;

tuned;

simplified exporter interface;

added implies_intr_goals;

tuned;

Tuned.

Removed exit command from end of main method.

PS method now calculates layout using default font metrics.

Inserted table for character widths.

tuned induction proofs;

dest_env: norm_term on rhs;

typedef: export result;

ignore typedef result;

declare projected induction rules stemming from nested recursion;

TypedefPackage.add_typedef_no_result;