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;

headers for document generation

Final mods for list comprehension

renamed code_gen to export_code

explizit dependencies

using canonical instantiation interface

Sup now explicit parameter of complete_lattice

turned locales intro classes

updated keywords

conciliated Inf/Inf_fin

type_check: tuned singleton funs case;

theory header: more precise imports;

Word/document/root.tex

new root.tex for HOL-Word

no_document for Infinite_Set, Parity

removed allpairs

removed allpairs - use list comprehension!

added header

* HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution

boolean algebras as locales and numbers as types by Brian Huffman

Made UN_Un simp

Use 376/377 specials for sendback markup

ML system provides get_print_depth;

fixed a bug in demult: -a in (-a * b) is no longer treated as atomic

removed obsolete ML bindings;

converted ex/MT.ML;

make HOL-ex earlier;

NAMED_CRITICAL;

removed stateful init: operations take proper theory argument;

removed dead code: const_typargs, num_typargs, init;

proper signature;

removed obsolete atp_method; ResHolClause.XXX_write_file: theory argument;

export more tactics; ResHolClause.literals_of_term: proper theory argument; removed obsolete ResClause.init, ResHolClause.init;

renamed ResAtpMethods.setup;

added at-poly-5.1-para;

added CRITICAL section markup;

updated generated file;