added global modes ref;

sane numerals (stage 3): provide generic "1" on all number types;

* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; note that these symbols are unavailable in Proof General / X-Symbol;

fixed numerals;

added tturnstile, TTurnstile;

*** empty log message ***

*** empty log message ***

replace 0r/1r by 0/1;

*** empty log message ***

fixed numerals;

* sane numerals (stage 2): plain "num" syntax (removed "#");

tuned;

*** empty log message ***

sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;

*** empty log message ***

"num" syntax;

added axclass "one" and polymorphic const "1"; print consts "0" and "1" with type constraints;

added "num" token;

induct: case names;

sane spacing of "-";

tuned;

Thm.major_prem_of part of Logic.strip_assums_concl;

major_prem_of: Logic.strip_assums_concl;

induct/cases made generic, removed simplified/stripped options;

improved proof by cases and induction;

removed obsolete comment;

generic induct_method.ML; tuned;

non-oriented infix = and ~= (output only); added case_split (with case names);

$(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;

use "~~/src/Provers/induct_method.ML";

removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);

added dest_concls;

simp_case_tac is back again from induct_method.ML; tuned;

made generic (see Provers/induct_method.ML);

qualify MetaSimplifier;

unsymbolized;

moved atomize stuff to theory IFOL; added induct/cases setup;

atomize stuff from theory FOL; tuned;

added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;

theory Natural_Numbers;

use "~~/src/Provers/induct_method.ML";

Theory of the natural numbers: Peano's axioms, primitive recursion. (Modernized version of Larry Paulson's theory "Nat".)

full_rewrite_cterm_aux (see also tactic.ML); no longer open MetaSimplifier;

added full_rewrite_cterm;

proof by cases and induction on types and sets (used to be specific for HOL);

qualify MetaSimplifier;

added dest_conj, dest_concls;

document setup;

added print_induct_rules;

tuned print operation;

tuned;

* moved induct/cases attributes to Pure, added 'print_induct_rules' command;

print_induct_rules;

updated;

Fixed bug in decompose.

Tools/induct_attrib.ML now part of Pure;

Isar/induct_attrib.ML;

*** empty log message ***

moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;

tuned parentheses in relational expressions;

moved linorder_cases to theory Ord;

linorder_cases supersedes linorder_less_split; tuned parentheses in relational expressions;

eta-expansion required for SML/NJ

support non-oriented infix;

tuned;

tuned;

*** empty log message ***

initial setup for chapter on document preparation;

updated output;

- declared wf_java_prog as syntax (previously: definition) - in wf_java_mdecl: added preconditions for 'This' - rule LAss: precondition v ~=This

Removed some unfoldings of defs after declaring wf_java_prog as syntax

Added axiom e~=This to reflect strengthened precond. in rule LAss

Minor modifications

added Ordinals example;

Tuned indentation of abstractions.

tuned;

inductive: no collective atts;

inductive: no collective atts;

oops;

tuned;

recdef (permissive); inductive: no collective atts;

*** empty log message ***

prove: ``strict'' argument;

internal thm numbering with ":" instead of "_";

avoid handle _;

permissive option;

inductive: no collective atts;

updated;

recdef (permissive);

Tuned section about parsing and printing proof terms.

mksimps and mk_eq_True no longer raise THM exception.

Added label for section on terms.

Added documentation for proof terms.

Added TYPE to Pure grammar.

Added \ttlbrack and \ttrbrack.

Added TPHOLs2000 paper about proof terms.

updated;

tuned;

tuned;

- Exchanged % and %%. - Fixed bug in shrink.

- Tuned syntax - proof_of_term: fixed problems with dummy patterns and typing information

- Exchanged % and %% - Renamed reconstruct_prf to reconstruct_proof

Exchanged % and %%.

HOL: eliminated global items;

updated;

eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");

renamed theory "subset" to "Typedef";

unsymbolize;

renamed "()" to Unity;

HOLogic.unit;

made unit type local;

tuned:

renamed "()" to Unity, made local;

added surjE;

prepared for Isabelle2001;

renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;

updated;

renamed real_of_int_eq_iff to real_of_int_inject;

document setup;

new-style theory;