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

move bool list operations from WordBitwise to WordBoolList

Word/WordBoolList.thy

move if_simps from BinBoolList to Num_Lemmas

Axioms for class no longer use object-universal quantifiers

move bool list stuff from WordDefinition and WordArith to new WordBoolList theory

move bool list stuff from BinOperations to BinBoolList; reorganize BinBoolList into subsections

Added mod cancellation simproc

remove redundant lemmas

declare conj_absorb [simp]

replace iszero_number_of_Pls with iszero_0 in rel_simps

add lemma of_int_power

Isar-style proof for lfp_ordinal_induct

ProofContext.restore_mode;

added inner syntax mode, includes former type_mode and is_stmt;

Modified message for sendback

"sendback" to PG for one-line proof reconstructions

Deleted the partially-typed translation and the combinator code. Minimize_applies now uses the same translation code, which handles both cases anyway.

move BIT datatype stuff from Num_Lemmas to BinGeneral

simplify termination proof

simplify proof of word_of_int

improved evaluation interface

moved ordered_ab_semigroup_add to OrderedGroup.thy

updated

move udvd, div and mod stuff from WordDefinition to WordArith

move order-related stuff from WordDefinition to WordArith

add lemma one_less_power

move scast/ucast stuff to its own subsection

move shifting-related constant definitions from WordDefinition to WordShift

use HOL-ex later;

standard_parse_term: added pp/check argument, include disambig here (from sign.ML);

inner syntax: added parse_term/prop;

read_def_terms: moved disambig to syntax.ML;

tuned CRITICAL sections;

remove redundant lemma int_number_of

AC rules for bitwise logical operators no longer declared simp

move bit simps from BinOperations to BitSyntax

minimize imports

reorganize into subsections

prepare_dummies: NAMED_CRITICAL;

with_modes []: non-critical;

tuned signature;

File.read/write/append: non-critical (basic IO operations already thread-safe);

TextIO.inputLine: non-critical (assume exclusive ownership);

tuned merge operations via pointer_eq;

cleaned up; declared more simp rules

issue a warning, when encountering redundant equations (covered by prece3ding clauses)

remove int_of_nat

remove int_of_nat; fix abs instance

use overloaded bitwise operators at type int

use class instead of axclass

theory header: fixed import;