fix occurences of numerals in HOL/ZF terms;

New lemmas by Stefan Merz.

avoid '(0 subgoals)';

Toplevel.excursion_error;

added exists;

Tuned.

a stronger diff_less and no more le_diff_less

removed 2 qed_goals

tweaked proofs to handle new freeness reasoning for data c onstructors

more existing theorems renamed to use #0; also new results

now exports mk_bin

a more robust proof

tweaked proof after removal of diff_is_0_eq RS iffD2

better error message for curried recdefs, etc.

Mod by Norber Voelcker

checkpoint;

Eliminated addDistinct.

facts: no statement_binds;

Datatype package now handles arbitrarily branching datatypes.

skeleton only;

added isar-ref;

Documented usage of function types in datatype specifications.

added attdx, methdx;

added isabelle_isar logo;

updated; tuned;

renamed 'with' to 'using';

*** empty log message ***

NatBin: binary arithmetic for the naturals

examples of arithmetic on the naturals

deleted a reference to "nat", now erroneous because "nat" is a function

many new laws about div and mod

new theorem zless_zero_nat

removal of rewrites for Suc(Suc(Suc...)))

NatBin: binary arithmetic for the naturals

getting rid of qed_goal

getting rid of qed_goal

new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m

Modifid length_tl

adapted to dest_keywords, dest_parsers;

separate command tokens;

tuned dest_lexicon;

tuned;

removed break;

removed BREAK, ROLLBACK;

structure LocalDefs = LocalDefs; structure Calculation = Calculation; structure SkipProof = SkipProof;

Exported function unify_consts (workaround to avoid inconsistently typed recursive constants in inductive and primrec definitions).

Added new example (infinitely branching trees).

Infinitely branching trees.

Replaced datatype_info by datatype_info_err.

- Now also supports arbitrarily branching datatypes. - Fixed bug (in some rare cases, recursive constants were inconsistently typed in different primrec equations).

- Datatype package now also supports arbitrarily branching datatypes (using function types). - Added new simplification procedure for proving distinctness of constructors. - dtK is now a reference.

Added some definitions and theorems needed for the construction of datatypes involving function types.

Some rather large datatype examples (from John Harrison).

improved print_thms;

export init_state; end_proof: reset goal_facts;

more renaming of theorems from _nat to _int (corresponding to a function that was similarly renamed some time ago Also new theorem zmult_int

more renaming of theorems from _nat to _int (corresponding to a function that was similarly renamed some time ago

qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int

qed_goal -> Goal

tuned;

tuned comments;

tuned contradiction method; improved comments;

improved comment;

more marg_comments;

Deriving rules in Isabelle;

rewrite add1_zle_eq is no longer in the default simpset

optimization for division by powers of 2

new montonicity theorems

new constant folding rewrites

handle cgoal;

added mk_cgoal, assume_goal;

same_tac;

change to force (m div 0 = 0)

many new theorems

renamed inj_nat to inj_int

new monotonicity theorems

new theorem zmult_eq_0_iff

renamed sort "numeral" to "number"

simplified the <= monotonicity proof

local qeds: print rule;

added show_hyps flag;

local qed; print rule;

term/prop: include number; method args: exlude method meta chars;

added show_hyps flag; local qed: print rule;

export assumption_tac; local qeds: print rule; same_tac: actually insert rules, !! bind vars;

removed merge_theories;

removed metacuts_tac;

tmp_path: *add* path;

thms_containing: undeclared consts error;

removed pretty_thm_no_hyps (again);

removed merge_theories;

may get BASH_PATH etc. from env;

new theorems for the "at most" relation

def: ==;

tuned Interrupt msgs;

pass exn;