suppress document output

theory with syntax for lattice operations

added babel -- necessary for bind infix syntax

added enumeration of predicates

moved instance option :: finite to Option.thy

constructive version of Cantor's first diagonalization argument

equalities for Min, Max

merged

added lemma

merged

Docs

eliminated Output.immediate_output -- violates the official message channel protocol;

schedule_seq: handle after_load errors as in schedule_futures;

replaced archaic use of rep_ss by Simplifier.mksimps;

improved error handling for document antiquotations;

merged

merged

Added "expect" option to Refute, like in Nitpick, that allows to write regression tests. Also replaced calls to "Output.immediate_output" with "priority" or "tracing", because "immediate_output" causes some problems (as explained by Makarius to Sascha).

added lemmas

Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead. I tested the affected symbols (card, finite, lfp, and gfp), and Refute now works better than before (i.e., more precision and more speed).

merged

merged

Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.

merged

merged

set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

merged

set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

tuned

moved complete_lattice to Set.thy

dropped Id

corrected slip in NEWS

merged

added strict_mono predicate

Identifiers of some old CVS file versions;

recovered generated files;

more precise deps;

merged

Added Docs

render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;

removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;

removed unused TableFun().fold_map and GraphFun().fold_map_nodes;

removed spurious occurrences of old rep_ss;

Thm.add_oracle interface: replaced old bstring by binding;

silent chmod;

Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;

close_schematic_term: uniform order of types/terms; tuned;

eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;

TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;

fixed proofs -- follow-up to ecd6f0ca62ea;

renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name"); tuned;

renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;

eliminated obsolete ProofContext.full_bname;

Binding.prefix_of;

adapted Binding.dest; tuned;

added prefix_of; tuned signature; tuned;

Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.

merged

declare power_Suc [simp]; remove redundant type-specific versions of power_Suc

regenerated document;

merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);

dummy changes to produce a new changeset of these files;

updated generated file -- changed since @{ML} now ignores source flag;

fixed document;

removed old/broken CVS Ids;

ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;

merged

Moved general theorems about sums and products to FiniteSet.thy

fixed proofs; added rules as default simp-rules

A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms

Added Libray dependency on Topology_Euclidean_Space

Added general theorems for fold_image, setsum and set_prod

fixed proofs

merged

merged

merged

merged

Second try at adding "nitpick_const_def" attribute. I don't know what happened the first time (change d8944fd4365e). It just vanished somehow.

Fix parentheses.

merged

Added "nitpick_const_simp" attribute to Nominal primrec.

NEWS: renamed o2s to Option.set;

less arbitrary occurrences of undefined

datatype antiquotation does not assume LaTeX as output any longer

merged

Option.thy

consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun

merged

explicit error message for `improper` instances lacking explicit instance parameter constants

Merge.

Merge.

Merge.

Made Refute.norm_rhs public, so I can use it in Nitpick.

Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.

Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number. I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it). These changes have no inpacts on already working Isabelle installations.

merged

Made Option a separate theory and renamed option_map to Option.map

renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);

eliminated internal stamp equality, replaced by bare-metal pointer_eq; misc tuning and polishing;

tuned str_of, now subject to verbose flag;

added @{binding} ML antiquotations;

added print_properties, print_position (again);

merged

merged

tuned manuals

more canonical directory structure of manuals

merged

removed and renamed redundant lemmas

renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;

moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings; moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names; type binding: maintain explicit qualifier, indepently of base name; tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused); Binding.str_of: include markup with position properties; misc tuning;

added markup for binding; tuned;

Binding.str_of; removed dead code; tuned;

Binding.str_of; pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;

Binding.str_of;

renamed Binding.display to Binding.str_of, which is slightly more canonical; tuned signature;

nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;

moved name space externalization flags back to name_space.ML; added pure version extern_flags; do not export internal get_accesses;

moved name space externalization flags back to name_space.ML; display: always show prefix for now; tuned signature;

reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);

merged

Thm.binding;

added type binding and val empty_binding;

updated generated files;

ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;

Implement Makarius's suggestion for improved type pattern parsing.

find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch

adapted to lates experimental version; PolyML.Compiler.CPPrintInAlphabeticalOrder false (redundant?);

removed Ids;

merged

reduced confusion code_funcgr vs. code_wellsorted

better markup

name fix

merged

name changes

Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy

fixed broken @{file} refs;

merged

using plain ISABELLE_PROCESS

merged

ignore ISABELLE_LINE_EDITOR for code generation

use long names for old-style fold combinators;

discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;

avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;

end_timing: generalized result -- message plus with explicit time values;

replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); minor tuning according to Isabelle coding conventions;

updated contributors;

removed parts of the manual that are clearly obsolete, or covered by newer manuals already (notably "isar-ref" or "implementation");

merged

minor update of Mercurial HOWTO;

removed redundant lemmas

added lemmas by Jeremy Avigad

A Serbian theory, by Filip Maric.

more accurate deps;

merged

add news for HOLCF; fixed some typos and inaccuracies

fixed headers;

moved isabelle_system.scala to src/Pure/System/;

moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);

updated generated files;

added method "coherent"; tuned formal markup;

more refs;

moved method "iprover" to HOL specific part;

removed Ids;

simultaneous use_thys;

replaced low-level 'no_syntax' by 'no_notation'; tuned header; tuned proofs;

moved generic intuitionistic prover to src/Tools/intuitionistic.ML;

tuned message;

* New prover for coherent logic (see src/Tools/coherent.ML).

more CONTRIBUTORS; fixed some dates;

removed Ids;

moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;

some updates on ancient README;

fixrec package uses new-style syntax and local-theory interface

add function taken_names

merged

make list-style polynomial syntax work when show_sorts is on

more CONTRIBUTORS;

turned "read-only refs" typ_level and minimize_applies into constant values;

merged

removed global ref dfg_format

removed local ref const_needs_hBOOL; renamed some const_min_arity parameters to cma

removed local ref const_min_arity

eliminated private clones of List.partition;

observe some Isabelle/ML coding conventions; avoid structure alias FT, which would complicate systematic searches unnecessarily;

eliminated NJ's List.nth;

tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;

tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;

observe basic Isabelle/ML coding conventions;

moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;

added ML-Systems/polyml-experimental.ML; more systematic treatment of bootstrap files;

tuned;

even less default memory for sunbroy2;

merged

merged

Made then_conv and else_conv available as infix operations.

merged

fixed typo

merged

avoid using legacy type inference

use TheoryData to keep track of pattern match combinators

merged

remove unnecessary simp rules

revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)

merged

back to canonical ROOT, to see if memory problems still persist;

trying less default memory for sunbroy2 test

basic setup for chapter "Syntax and type-checking";

merged

standard headers; eliminated non-ASCII chars, which are fragile in the age of unicode;

updated generated files;

uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities; more robust handling of "|" within index;

fixed import of ~~/src/HOL/Decision_Procs/Ferrack;

more explicit indication of old manuals;

merged

\bibliographystyle{abbrv} for newer ref manuals;

added Haftmann-Wenzel:2009;

updated generated files;

isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;

merged

include HOL-Decision_Procs in stats;

back to plain http;

merged

Added postprocessing rules for fresh_star.

Fixed nonexhaustive match problem in decomp, to make it fail more gracefully in case assumptions are not of the form (Trueprop $ ...).

tuned NEWS;

merged

merged

add type annotation

disable floor_minus and ceiling_minus [simp]

merged

merged

Updated the theory syntax. Corrected an error in a command.

merged

generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono

new theory of Archimedean fields

add lemmas about comparisons of Fract a b with 0 and 1

merged

add lemma diff_Suc_1

Added lemmas for normalizing freshness results involving fresh_star.

Added typing and evaluation relations, together with proofs of preservation and progress (i.e. part 2A of the POPLmark challenge).

merged

Use LocalTheory.full_name instead of Sign.full_name, because the latter does not work properly for locales.

Replaced Logic.unvarify by Variable.import_terms to make declaration of equivariance lemmas work in locales.

nominal_inductive and equivariance now work on local_theory.

Added equivariance lemmas for fresh_star.

NEWS

merged

robustified

make more proofs work whether or not One_nat_def is a simp rule

add simp rules for numerals with 1::nat

fix lemma hypreal_hnorm_def

make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules

move lemma dvd_mod_imp_dvd into class semiring_div

merged

improved treatment of case certificates

repaired order of variable node allocation

explicitly import Fact

change imports to move Fact.thy outside Plain

add lemmas poly_{div,mod}_minus_{left,right}

merged

declare scaleR distrib rules [algebra_simps]; cleaned up

clean up instantiations

merged

simplify some proofs

remove duplicate instance declaration

stripped classrels_of, instances_of

use canonical subalgebra projection

experimental switch to new well-sorting algorithm

handle NONE case in arity function properly

clarified status of variables in evaluation terms; tuned header

subalgebra: drop arities if desired

merged

more liberality needed

merged

added lemmas

merged

simplified evaluation

merged

added dvd_div_mult

merged

first attempt to solve evaluation bootstrap problem

formal dependency on newly emerging algorithm

merged

name fix

fix spelling

real_inner class instance for vectors

NEWS

merged

Removed subsumed lemmas

remove duplicated lemmas about norm

real_normed_vector instance

fix real_vector, real_algebra instances

merged

generalize lemmas from nat to 'a::wellorder

generalize some lemmas

merged

removed redundant thms

merged

class instances for num1

Removed redundant lemmas

merged

also consider superclasses properly

merged

removed subsumed lemmas

merged

datatype antiquotation: always bracket types with spaces in between

consequent use of term `code equation`

permissive check for pattern discipline in case schemes

maintain order of constructors in datatypes; clarified conventions for type schemes

stripped Id

merged

add theory of products as real vector spaces to Library

add new theory Product_plus.thy to Library

merged

changed message

detailed information on atp-failure via Output.debug

merged

reverted to old wellsorting algorithm

fixed spurious proof failure

consider changes variable names in theorem le_imp_power_dvd

tuned and incremental version of wellsorting algorithm

ignore sorts in bare types

defensive implementation of pretty serialisation of lists and characters

dropped Id

experimental inclusion of new wellsorting algorithm for code equations

merged

merged

merged

fixed selection of premises

cleaned up

declare of_int_number_of_eq [simp]

fix case_names

nicer induction/cases rules for numeral types

number_ring instances for numeral types

declare xor_compl_{left,right} [simp]

add rule for minus 1 at type bit

add formalization of a type of integers mod 2 to Library

new theory of real inner product spaces

add Powerdomain_ex.thy

add more ordering lemmas

avoid using ab_semigroup_idem_mult locale for powerdomains

merged

add header

move Polynomial.thy to Library

move FrechetDeriv.thy to Library

split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy

half auto_solve default time out; increase manually in PG for large projects (L4v/Verisoft large).

merged

finish converting Deriv.thy to new polynomial library

generalize int_dvd_cancel_factor simproc to idom class

composition of polynomials

add some lemmas, cleaned up

generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power

move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial

merged

more subsection headings

speed up proof of exp_exists

tuned

sort instances wrt. to class hierarchy

fixed signature

tuned accessor name

more precise improvement in instantiation user space type system

do not drop arguments to 0, 1

merged

reverted to previous version of Finite_Set.thy

merged

merged

first working version

tuned comments, stripped ID, deleted superfluous code

stripped ID

Syntactic support for products over set intervals

No idea what happened here!

Even and odd powers of -1

merged

Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

Added Nitpick tag to 'of_int_of_nat'. This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.

add lemmas for exponentiation

merged

unified variable names in case expressions; no exponential fork in translation of case expressions

merged

remove redundant simp attributes for zdvd rules

lemmas abs_dvd_iff, dvd_abs_iff

Cleaned up IntDiv and removed subsumed lemmas.

tune section headings; add square function

merged

rearrange subsections

remove instances num::semiring and num::linorder

datatype num = One | Dig0 num | Dig1 num

replace 1::num with One; remove monoid_mult instance

replace dec with double-and-decrement function

more default simp rules for sgn

re-generated

clarified import

faster preprocessor

added pdivmod on int (for code generation)

merged

tuned texts

dropped Id

dropped clause_suc_preproc for generic code generator

new primrec

Adapted to encoding of sets as predicates.

enable auto-solve by default

merged

Added nitpick attribute, and fixed typo.

Added myself to testing list.

dvd and setprod lemmas

merged

added finite_set_choice

reject defined function in patterns with errmsg, e.g. f (f x) = x

fixed document

more finiteness

merged

more finiteness

merged

more finiteness

generalize lemma fps_square_eq_iff, move to Ring_and_Field

generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup

add mult_delta lemmas; simplify some proofs

fix spelling

declare fps_nth as a typedef morphism; clean up instance proofs

add lemma surj_from_nat

fix document generation

merged

fix document generation

section -> subsection

add instance for cancel_comm_monoid_add

add class cancel_comm_monoid_add

more finiteness changes

merged

finiteness lemmas

merged

unset execute bit

Tuned datatype antiquotation.

made SMLNJ happy

typo

find_consts: display the search criteria. (by Timothy Bourke)

find_consts: documentation. (by Timothy Bourke)

FindTheorems solves: update documentation (by Timothy Bourke)

fixed codegen tool

merged

fixed codegen tool

merged

Moved Nat_Int_Bij into Library

removed Reflection session

add lemma add_nonneg_eq_0_iff

add lemmas about sgn

added ML file for the find_consts command

added find_consts to NEWS and CONTRIBUTORS

New command find_consts searching for constants by type (by Timothy Bourke).

fix document generation

move countability proof from Rational to Countable; add instance rat :: countable

Moved FTA into Lib and cleaned it up a little.

ordered_idom instance for polynomials

Export tactic interface for sizechange method

merged

liberal inst_meet

display code theorems with HOL equality

merged

Added serial_string to SAT solver input and output files, to prevent multithreading chaos. Bug reported by Tobias.

Added nitpick_const_simp attribute to recdef and record packages.

Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.

Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.

Reintroduced nitpick_ind_intro attribute. It looks like I need it nonetheless.

merged

Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.

merged

Merged.

Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.

fixed typo

updated NEWS etc with "solves" criterion and auto_solves

merged

Moved Order_Relation into Library and moved some of it into Relation.

Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke

FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke

const_name antiquotations

Repaired a proof that did, after all, refer to the theorem nat_induct2.

merged

Strengthened the induction rule nat_induct2.

Deleted the induction rule nat_induct2, which was too weak and not used even once.