removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;

added singleton check_typ/term/prop;

removed obsolete read/cert variations (cf. Syntax.read/check);

replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

replaced ProofContext.read_term/prop by general Syntax.read_term/prop;

*** empty log message ***

final(?) iteration of sgn saga.

reject_vars: accept type-inference params; standard_term_check: include prepare_pattern; infer_type: mode_schematic; tuned;

exported is_param;

legacy_infer_term: ProofContext.mode_schematic;

prove: setmp quick_and_dirty (avoids race condition);

export various inner syntax modes; Syntax.add_term_check: include expand_abbrevs (consts and var bindings);

type_infer: mode_pattern;

do not touch quick_and_dirty;

tuned multithreading entry -- no longer experimental;

explained \isatstyle(minor)

added short_names explanation

added join_mode; expand_binds: mode dependent; removed infer_types(_pat) -- use general Syntax.check_terms instead;

replaced ProofContext.infer_types by general Syntax.check_terms; use Variable.polymorphic to get schematic type variables;

replaced ProofContext.infer_types by general Syntax.check_terms;

*** empty log message ***

added constant sgn

added lemma

added some more entries;

turned type_check into separate typ/term_check; tuned sifnature;

tuned;

moved type_mode to type.ML; Syntax.add_typ_check;

infer_types: general check_typs instead of Type.cert_typ_mode;

maintain mode in context (get/set/restore_mode);

added burrow_types;

- tuned section about inductive predicates - fixed broken railroad diagram in section about executable code

ported div/mod simprocs from HOL/ex/Binary.thy

renamed POLYML_LINK_OPTIONS to POLY_LINK_OPTIONS;

added POLYML_LINK_OPTIONS, which is required for unusual platforms (notably cygwin);

some simultaneous use_thys;

Updated section about inductive definitions.

turned list comprehension translations into ML to optimize base case

added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);

added x86-solaris;

fixed Proofs

added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);

removed unused theorems ; added lifting properties for foldr and foldl

removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);

Deleted unused fillin_mixfix function.

mark all parallel sessions as experimental

atbroy99 is 64bit

fixed pattern comnpletion; untabified

revert to Word library version from 2007/08/20

TheoremHook: fixed copy-paste mistake;

Smaller size and fewer iterations for quickcheck.

codegen.ML is now loaded in Pure again.

Changed "code" attribute of concat_map_singleton to "code unfold".

Code generator now uses sequences with depth limit.

Got rid of large simpset in proof of characteristic equations for freshness.

Added sequences with recursion depth limit.

Adapted to changes in interface of Specification.theorem_i

- restored old setup - new infrastructure for auto quickcheck - fixed bug in eta_expand that caused argument types to get mixed up

codegen.ML is now loaded in Pure again.

- new auto-quickcheck flag - repaired and inserted proof_pref again

Added local_theory_to_proof'

- theorem(_i) now also takes "interactive" flag as argument - added theorem hook

Specification.theorem now also takes "interactive" flag as argument.

Commented out non-standard paragraph formatting.

added (code) lemmas for setsum and foldl

replaced 'sorry' by unproven;

do not touch quick_and_dirty;

norm_absolute: CRITICAL;

tuned load order -- minimizes modules before Secure;

induct: proper separation of initial and terminal step; avoid unspecific prems;

move WordExamples to Examples directory

HOL-Word-Examples

Word Examples directory

add parallel sessions for atbroy99 and macbroy6

HOL_USEDIR_OPTIONS: no special -M setting (now works with multithreaded);

Added infinite_descent

updated keywords

added code_props

introduces params_of_sort

added simple definition scheme

added explicit equation for equality of nested environments

circumvented infix problem

tuned linear arith (once again) with ring_distribs

made SML/NJ happy

described 'rotated' attribute

made SML/NJ happy

revised blacklisting for ATP linkup

new derived rule: incr_type_indexes

Returning both a "one-line" proof and a structured proof

Reconstruction bug fix

overloaded definitions accompanied by explicit constants

moved class dense_linear_order to Orderings.thy

updated

made sets executable

remove unused lemmas

bin_sc_nth proof

remove lemma bin_rec_PM

avoid use of bin_rec_PM

new instance proofs

remove unused lemmas

import BinInduct; remove constant bin_rl; remove redundant lemmas and definitions; clean up some proofs

declare bin_rest_BIT_bin_last [simp]

Word/BinInduct.thy

theory of integers as an inductive datatype

move bin_nth stuff to its own subsection

removed Word/Size.thy; replaced len_of TYPE('a) with CARD('a); replaced axclass len with class finite; replaced axclass len0 with class type

typed print translation for CARD('a); declare zero_less_card_finite [simp]

rename type pls to num0

move constant definitions to their respective subsections

tuned;

More selective generalization : a*b is generalized whenever none of a and b is a number

imports Presburger; no need for Main