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;

revisions e.g. images, transitive closure...

*** empty log message ***

*** empty log message ***

case_tac on bools

case_tac subgoals

deleted the obsolete nat_neqE (and reformatting)

deleted the obsolete nat_neqE

generalizing the LEAST theorems from "nat" to linear orderings and wellorderings

now using "by" for one-line proofs

various changes including the SOME examples, rule_format and "by"

loads the new theory

reformatting, and splitting the end of "Primes" to create "Forward"

*** empty log message ***

now using "by" for one-line proofs

introduction of "by" and a few examples of SOME

auto update

new wfrec example

fixed the treatment of Rules and Sets

*** empty log message ***

use \<acute>;

added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;

added acute, cedilla, dieresis, hungarumlaut;

` -> $

*** empty log message ***

`` -> ` and ``` -> ``

`` -> and ``` -> ``

replaced \<macron> by \<inverse>;

avoid renaming of params in cases;

split_all operation;

improved evaluation judgment syntax; modified Loop rule

syntax (xsymbols);

Removed Applyall

additional pattern allows reduction of fractions to lowest terms

*** empty log message ***

updated;

removed ID (avoid CVS conflicts with generated versions);

CHANGED_PROP;

removed MicroJava/BV/Convert.thy;

do not AutoBind.drop_judgment;

tuned output;

tuned norm_hhf(_tac);

added is_norm_hhf;

removed outdated comment;

case binds: AutoBind.drop_judgment;

tuned split_all_tac;

merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)

support ?case binding; tuned;

apply_case: more robust handling of bounds; moved norm_hhf to Pure/tactic.ML;

moved norm_hhf_tac to Pure/tactic.ML; adapted invoke_case;

added drop_judgment;

export read_inst', inst'; tuned;

added list_abs;

added norm_hhf(_tac);

Tactic.norm_hhf;

'of:' params spec; tuned;

'cases' / 'induct' method: ?case binding, 'of:' spec;

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

^^ -> ``` Univalent -> single_valued

Fleuriot reference

minor edits to Chapters 1-3

revisions especially concerning the reals

*** empty log message ***

a few extra brackets

*** empty log message ***

*** empty log message ***

Changed priority of dvd from 70 to 50 as befits a relation.

*** empty log message ***

new UNITY examples by Sidi Ehmety

Field of a relation, and some Domain/Range rules

finite_trancl: new theorem by Sidi Ehmety

more removal of obsolete rules

fixed two proofs that were affected by the removal of obsolete rules

new examples by Sidi Ehmety

tuned comment;

renamed .sml files to .ML;

label!

more tidying, especially to remove real_of_posnat

initial material on the Reals

updated;

added recdef_tc(_i);

recdef_tc;

renamed .sml files to .ML; tuned package setup;

TFL: renamed .sml to .ML;

added 'recdef_tc' command;

* Isar/HOL: added 'recdef_tc' command;

renamed .sml files to .ML; proper handling of Isabelle exceptions; tuned;

tuned;

Thm: dest_comb, dest_abs, capply, cabs no longer global;

removal of the nat_cancel_factor simproc

Types chapter now uses HOL-Real

some HOL-Real material

added type annotation to Call

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

minor tidying of simprocs

put in some missing Hyperreal files

Hyperreal

separation of HOL-Hyperreal from HOL-Real

now #16*(x+y) distributes for nat just as for other numeric types

a generic ordering theorem used in Real

tidying, and separation of HOL-Hyperreal from HOL-Real

separation of HOL-Hyperreal from HOL-Real

separation of HOL-Hyperreal from HOL-Real

recover: ignore result;

recover: malformed result;

scan: malformed result;

recover: result;

proper error msg;

'erule' etc.: assm arg;

Method.erule 0;

updated;

'insert' made proper; 'erule' etc.: assm arg;

ares_tac, [edf]atac;

antiq: preview errors;

tuned length;

tuned output;

recover_order for single step tules;

simplified quick_and_dirty stuff; tuned;

tuned;

hide type node item;

Tools/string_syntax.ML;

tuned comment;

SML90 stuff;

handle proper rules;

export rewrite_cterm;

added inductive_conj;

tuned;

better definitions of SML90 features

*** empty log message ***

something stopped working, had to add real_add_ac

rational linear arithmetic

this makes the proof run (or run faster)

further tidying of NSA proofs

*** empty log message ***

rational arithmetic

rational arithemtic

re-orientation of integer literals

more tidying, especially to rationalize the simprules

re-orientation of 0=... (no idea why the backslashes have changed too)

simproc bug fix: negative literals and large terms

further tidying

generalized the re-orientation 0f 0=... to all types

tidying, removing obsolete lemmas about 0=... and 1=...

tidying, removing obsolete lemmas about 0=...

SML90: ord, chr, explode, implode;

re-orienting equations with #nnn on the lhs

re-orienting equations with 0, 1, 2 on the lhs

new file extract_common_term.ML for the cancel-factor simprocs

inserting the simproc nat_cancel_factor

inserting the simproc int_cancel_factor

new simprule zero_less_abs_iff

coping with the re-orientation of #nn=x

cancel-factor simproc allows shorter proofs

more tidying

cancel-factor simproc allows a shorter proof

improved errors;

*** empty log message ***