added spaces; added default_indent, indent;

support general indentation (e.g. for non-tt latex output); tuned;

added replicate_string;

updated;

\isaindent;

tuned;

Ring_and_Field_Example;

instance int :: ordered_ring moved to Ring_and_Field_Example, because it changes the way that int expressions get simplified, violating the strict library principle (cf. README.html);

added Library/Ring_and_Field_Example.thy;

*** empty log message ***

added HOL/Library/Nested_Environment.thy;

updated;

more bugs;

forget RPM;

convert legacy tactic scripts to Isabelle/Isar tactic emulation;

made SML/XL happy;

tuned;

show(_i): check goal;

show/thus: check_goal;

show/thus: Toplevel.proof';

infix \\\\;

added exists_stamp; added PureN, CPureN;

use Sign.PureN, Sign.CPureN;

Sign.exists_stamp;

tuned \<And> and \<Or>;

generate index.html for pdf docs;

splitted Loop rule

removed redundant proof

is_class and class now as defs (rather than translations); corrected Digest.thy

use_output: proper handling of non-ASCII symbols;

export plain_output;

Store.thy is obsolete (newref isn't used any more)

removed obsolete MicroJava/JVM/Store.thy

newref -> new_Addr

renamings: real_of_nat, real_of_int -> (overloaded) real inf_close -> approx SReal -> Reals SNat -> Nats

renamed Product_Type.split to split_conv;

use Syntax.read_xnum;

tuned examples;

* HOL/datatype: induction rule for arbitrarily branching datatypes is now expressed as a proper nested rule (old-style tactic scripts may require atomize_strip_tac to cope with non-atomic premises); * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule to "split_conv" (old name still available for compatibility); * HOL: improved concrete syntax for strings (e.g. allows translation rules with string literals);

use_text etc.: proper output of error messages;

export fold_ast etc.;

removed Session.finish ();

proper induction rule for arbitrarily branching datatype;

export inductive_forall_name, inductive_forall_def, rulify;

improved string syntax (allow translation rules);

renamed Abs_Node_inject to Abs_Node_inj;

added atomize_strip_tac;

tuned atomize;

-f option;

removed;

removed ex/StringEx.ML;

split_conv;

updated;

isabelle -f;

more method_setup examples;

lcp's pass over the book, chapters 1-8

removed instructions Aconst_null+Bipush, introduced LitPush

tuned

*** empty log message ***

use_text_verbose: priority output;

use_mltext: priority output;

HOLogic.dest_binum; avoid handle _ !!!

hide dest_bin;

HOLogic.dest_binum;

wrong font for braces

LateX-2e moans about using \\choose

the \\epsilon character causes font errors in a section title

made SML/NJ happy;

lcp's pass over the book, chapters 1-8

renaming of some files

updated for new version of even-examples.tex

updated for new version of advanced-examples.tex

abs and other small changes

updated for new version of numerics.tex

renaming to avoid clashes

auto update

general revisions

added Sigma_Algebra;

added Induct/Sigma_Algebra.thy;

tuned;

do not hilite "xnum";

make_raw: do not AutoBind.drop_judgment;

induct cases: RuleCases.make_raw;

added strict_prefixI', strict_prefixE';

subst syntax;

*** empty log message ***

lcp's suggestions for CTL

*** empty log message ***

a new label

revisions corresponding to the new version of sets.tex

Added <cdot> syntax for continuous application $.

isatool unsymbolize;

updated;

tuned \DOT, \DDOT;

added \<wrong> symbol;

tuned;