tuned msg;

Added constant abs.

simprocs now simplify the RHS of their result

new lemmas about binary division

Added AVL

if_weak_cong should make linear arithmetic faster

a safer way of proving literal equalities

from Suc...Suc to #m

of course it should use Main

new lemmas concerning powers and #mmm

changed 2 to #2

Suc 0 -> 1

card_Pow is no longer a default simprule because it uses unary 2

simprocs

further tidying of integer simprocs

removed obsolete simproc combine_coeff

Installation of CombineNumerals for the integers Many bug fixes Removal of AssocFold for addition (nat and int)

removed obsolete simprocs

removed obsolete "evenness" proofs

TEMPORARY REMOVAL OF TWO BROKEN EXAMPLES

modified for new simprocs

now using binary naturals

various bug fixes

Cassini identity is easier to prove using INTEGERS

a more modern proof

now with combine_numerals

combine_numerals replaces both fold_Suc and combine_coeff

new simproc, replacing combine_coeffs and working for nat, int, real

signature change

inserted triviality check

*** empty log message ***

new, but still slow, proofs using binary numerals

[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist

number_of now takes a type arg

this change saves 15 seconds

bug fixes to new simprocs

[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist

removed some duplication, etc.

now uses the new cancel_numerals simproc

Provers/Arith/inverse_fold.ML is already obsolete

cleaner exceptions

now works for coefficients, not just for numerals no longer works by subtraction, so no need for inverse_fold

new file containing simproc invocations, from NatBin.ML

moved the simproc code to NatSimprocs.ML

Provers/Arith/inverse_fold.ML is already obsolete

new file Integ/NatSimprocs.ML

Provers/Arith/inverse_fold.ML is already obsolete Integ/NatSimprocs.ML added

*** empty log message ***

*** empty log message ***

TuturialI;

*** empty log message ***

check_file: keep expanded (!) absolute path;

Adding generated files

*** empty log message ***

fixed -c default value;

Adding generated files.

I wonder which files i forgot.

*** empty log message ***

I wonder if that's all?

deleted obsolete lemma_not_leI2

removal of less_SucI, le_SucI from default simpset

replaced obsolete diff_right_cancel by diff_diff_eq

added number_of_const: term

tidied

instantiates new simprocs for numerals of type "nat"

new simprocs for numerals of type "nat"

emilimated global names;

removed obsolete "simpset" keyword;

renamed 'hide' to 'hide_action';

fixed theory deps;

made SML/NJ happy;

made SML/NJ happy;

* improved name spaces: ambiguous output is qualified; support for hiding of names;

improved output of ambiguous entries; support hiding;

Pretty.chunks;

'global' / 'local': comment; added 'hide';

name space hide operations;

global/local_path: comment; added name space hide;

added 'hide';

tuned msg;

NameSpace.is_qualified;

Pretty.chunks;

mod to error msg

next_block: reset_facts;

plain ASCII;

intrn_arity: reject type abbreviations;

added is_type_abbr;

\newenvironment{isabellequote};

global \isa@parindent, \isa@parskip; \newcommand{\isa};

use HOLogic.termT;

outer syntax: no simps;

recdef: no simps;

stopped using the obsolete "nat_ind_tac"

added some new iff-lemmas; removed some obsolete thms

tidied

tuned;