Moved symbol.ML to front of file list (due to quote function).

first version of matrices for HOL/Isabelle

Added theory with examples for quickcheck command.

lemma drop_Suc_conv_tl added.

simplified ML code for setsubgoaler;

tuned document;

add locales

Zur Freude von Sebastian Skalberg!

Added Locales Tutorial.

say how to install PG and poly

fix cvs id

describe how to work on Isabelle repository version

make weblint happy

updated, tuned

*** empty log message ***

tuned;

session graph;

tuned document;

add feature list

add faq

add link to FAQ

add Isabelle2003 to archive

tuned;

fixed width; tuned;

finalconsts RepC AbsC;

Added ex/Exceptions.thy

"haspref" -> "oldhaspref" (David Aspinall)

bugfix in xsymbols_output

corrected PG url in comment

use more symbols in HTML output

renamed have_thms to note_thms;

tuned;

proper handling of lines terminated by CRLF or CR;

* raw control symbols are of the form \<^raw:...> now. * again allowing symbols to begin with "\\" instead of "\" for compatibility with ML-strings of old style theory and ML-files and isa-ProofGeneral.

Fixed bug in check_mode_clause.

bugfix for \<^raw...> scanner

prod and sum

* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in the scanner * output functions default_output and xsymbols_output only print one "\" for symbols (to be consistent with the scanner).

* Calculation commands "moreover" and "also" no longer interfere with current facts ("this"), admitting arbitrary combinations with "then" and derived forms.

'also'/'moreover': do not interfere with current facts, allow in chain mode;

export put_thms; do not export use_facts, reset_facts;

Added brief intro text.

convert symbols to HTML 4.0 character entities, convert some common remaining symbols to ASCII (e.g. lbrakk -> [|)

Various changes to HOL-Algebra; Locale instantiation.

hence -> from calculation have

fix moreover/this behaviour: "this" after moreover/also is not = calculation, but remains unchanged.

export thisN

isabelle.css

use .jar

change order of options for jar (fix error on Sun)

ignore GraphBrowser.jar

remove MiniML and Lex (moved to AFP)

use css in generated web pages

use css use Graphrowser.jar instead of .class files

use css use Graphbrowser.jar instead of .class files

produce jar instead of single .class files

removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy

added theorem chg_map_other

added HOLCF/Streams.thy (with concatenation etc.)

added Streams.thy (with stream concatenation etc.)

treat sub/super scripts

freeness theorems and induction rule

tidied

new theory

some (much longer) structured proofs

fix time tag of session.tex

Locale instantiation: label parameter optional, new attribute paramter.

IsaMakefile

new

*** empty log message ***

*** empty log message ***

new

*** empty log message ***

*** empty log message ***

Whoops. Those default cases can be tricky.

Added support for the newer versions of SML/NJ, which break several of the old interfaces.

Added a number of explicit type casts and delayed evaluations (all seemingly needless) so that SML/NJ 110.9.1 would accept the importer...

exposed fast_arith_neq_limit

Added HOL proof importer.

Tools/sat_solver.ML and Tools/prop_logic.ML added

fixed dpll solver (now uses NNF)

- Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>

variable renamings and other cosmetic changes

updated treatment of znegative and nat_of

introduced fast_arith_neq_limit

got rid of ignore_neq again.

Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>

ignore_neq also influences arith_tac now, not just fast_arith_tac

Added ignore_neq flag.

removal of Binary Trees examples prepratory to its going into AFP

new type class abelian_group

Added check that Theory.ML does not occur in the files section of the theory Theory.

Lex now in AFP

HOL/Lex is now in AFP/Functional-Automata

new

new

Added PSV 2003/2004

tidied

tidied

Added append_eq_append_conv2

Added bitvector library (Word) to HOL/Library and a theory using it (Adder) to HOL/ex.

include exercises again

removed intro to isabelle

put in sections, reorganized, removed intro to isabelle

allow sections in contents file

satsolver=dpll

slightly different SAT solver interface

Installed solvers now determined at call time (as opposed to compile time)

symbols in idents

new material from Avigad

new treatment of equivalence classes

documented new identifier syntax

moved MiniML and AVL to archive of formal proofs

auto update

clarified

streamlined treatment of quotients for the integers

added a few 0 and Suc lemmas

conversion of Hyperreal/Lim to new-style

removed redundant thms

new thms

New simplification ordering to move numerals together. Fixes a bug in the nat cancellation simprocs

stylistic tweaks

Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.

case_tac no longer raises THM exception if goal number is out of range.

auto update

heavy tidying

heavy tidying

new lemma

more up-to-date error msg

\<dots> replaced by ...

refute

Documentation updated

Refute_Examples added/fixed

look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only if no multi platform installation found.

SML/NJ compatibility fixes

added Refute_Examples.thy

changed default values for refute

*** empty log message ***

support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps

Updated examples

*** empty log message ***

Internal and external SAT solvers

Formulas of propositional logic

ZCHAFF_HOME variable added

new thm

strengthened the axclass claims

suggest -p 1 proof object level for HOL

include more explanation of variables

*** empty log message ***

Bug-fixes for transitivity reasoner.

Added documentation for transitivity solver setup.

generic theorems about exponentials; general tidying up

new theory of infinite sets

Lex: removed last ML files

Conversion ML -> Isar

tweaked for times_ac1

tweaks

some new results

some new results

Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal

patch to NumberTheory problems caused by Parity

do not remove heaps, used for afp test

Lex: ML -> thy

ML -> Isar

new material from Avigad, and simplified treatment of division by 0

Removed ML files from Lex

Conversion of ML files to Isar.

added record_ex_sel_eq_simproc

fixed bugs in the setup of arithmetic procedures

converted Hyperreal/IntFloor to Isar script

tuned. proofs still gruesome..

converted MiniML to Isar

converted to Isar

new Ring_and_Field hierarchy, eliminating redundant axioms

converted Hyperreal/HTranscendental to Isar script

converted to Isar

union/intersection over intervals

Added specific code generator for number_of.

converted Hyperreal/Series to Isar script

converted Hyperreal/NatStar to Isar script

corrected authors

converted Hyperreal/HSeries to Isar script

find_tname now handles parameter renaming properly ("as they are printed").

converted Hyperreal/Log and Hyperreal/HLog to Isar scripts

converted NSCA to Isar script

converted HOL/Complex/NSInduct to Isar script

converted HOL/Complex/NSCA to Isar script

conversion of Complex/CStar to Isar script

conversion of Complex/CSeries to Isar script

conversion of Complex/CLim to Isar script

Transitive_Closure: added consumes and case_names attributes Isar: fixed parameter name handling in simulatneous induction which I had not done properly 2 years ago.

new "where" section

moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy

removal of the legacy ML structure List

new numerics section using type classes

New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.

Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.

moved list_all2I to List.thy

removed a reference to the ML structure List.thy

new theorem

comments!!

new Union syntax

removed obsolete theorem

Moved application of flexflex_unique from standard' to standard.

further tweaks to the numeric theories

arith

lemmas about card (set xs)

Polymorphic treatment of binary arithmetic using axclasses

Removed dangling exception handler

Missing } inserted

Removed "duplicate fact binding" error message.

Printing functions now use cond_extrn instead of extrn (due to short_names flag)

Added flag short_names

Modified UN and INT xsymbol syntax: made index subscript

*** empty log message ***

updated links to the old ftp site

generic of_nat and of_int functions, and generalization of iszero and neg

tidying up, especially the Complex numbers

Changed variable names.

*** empty log message ***

further tidying of the complex numbers

tidying of the complex numbers

Finally fixed the counterexample finder. Can now deal with < on real.

Conversion of HyperNat to Isar format and its declaration as a semiring

simplifications in the hyperreals

tidying up arithmetic for the hyperreals

converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.

remove more files (index, log files) for -c option

replacing HOL/Real/PRat, PNat by the rational number development > of Markus Wenzel

replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel

\<^raw...> does no longer print an additional space.

Reduced space for xsymbols output of [| |] ==> from 3 to 1

\\<...> will be converted to \<...> \\<^...> will be converted to \<^...>

* Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy

Added an exception handler and error msg.

Added print translation for pairs

cleaning up

print translation for ALL x <= n. P x

fixed old bugs in "decomp" (conversion from term to lin.arith. format). updated instantiation of real lin.arith.

Told linear arithmetic package about injections "real" from nat/int into real.

types complex and hcomplex are now instances of class ringpower: omitting redundant lemmas

Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers

Modified real arithmetic simplification

Fixed compatibility issues with SML/NJ: - replaced '(op *)' by 'op*' - replaced 'LargeInt' by 'Int'

Adding 'refute' to HOL.

'refute', 'refute_params'.

Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal

set isasep to {} by default

Added lazy sequences and parser combinators for same.

separate thm lists in latex output by \isasep

run makeindex if necessary

map_idI

auto update

Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.

correction to cterm_instantiate by Christoph Leuth

*** empty log message ***

*** empty log message ***

undid split_comp_eq[simp] because it leads to nontermination together with split_def!

Deleting more redundant theorems

conversion of Real/PReal to Isar script; type "complex" is now in class "field"

tweaking of lemmas in RealDef, RealOrd

\<^bsub> .. \<^esub>

spanning super and sub scripts \<^bsub> .. \<^esub> and \<^bsup> .. \<^esup>

re-organized numeric lemmas

Added trace msg

re-organized some hyperreal and real lemmas

list_all2_nthD no good as [intro?]

list_all2_mono should not be [trans]

reorganised complex arithmetic

removing real_of_posnat

converting Hyperreal/NthRoot to Isar

converting Complex/Complex.ML to Isar

deleting redundant theorems

new theorems

tidying up hcomplex arithmetic

renaming some theorems

type hcomplex is now in class field

more ML bindings

added some [intro?] and [trans] for list_all2 lemmas

Updated proofs due to changes in Set.thy.

converted Complex/NSComplex to Isar script

removal of the abel_cancel simproc for hypreal

downgrading abel_cancel

new binding

simplifying

moving HyperArith0.ML to other theories

removing obsolete bindings

tidying of HOL/Auth esp Guard lemmas

removed insert_Diff_single from simpset because it interfered with Auth :-(

tidying first part of HyperArith0.ML, using generic lemmas

minor tweaks

type hypreal is an ordered field

*** empty log message ***

tidied

*** empty log message ***

converted Hyperreal/HyperDef to Isar script

fixed PG link

converted Hyperreal/HyperOrd to new-style theory

updated references to the now-pornographic proofgeneral.org

more general lemmas for Ring_and_Field

absolute value theorems moved to HOL/Ring_and_Field

moving some division theorems to Ring_and_Field

changed proof general links

Change to prune_prems in Pure/Isar/locale.ML.

removal of abel_cancel from Real

combining Real/{RealArith0,real_arith}.ML

Moving some theorems from Real/RealArith0.ML

Isar: where attribute supports instantiation of type variables.

New structure "partial_object" as common root for lattices and magmas.

Isar: where attribute supports instantiation of type vars.

re-organisation of Real/RealArith0.ML; more `Isar scripts

moreover and also do not reset facts any more

do not reset facts ('this') for moreover and also

make Pure first to avoid race conditions on multiprocessor machines

revert to 1.18, changed Distribution/lib/Tools/makeall instead

make Pure first to avoid race conditions on multi processor machines

Added lazy sequences and parser combinators for same.

more field division lemmas transferred from Real to Ring_and_Field

stylistic changes

Converting more of the "real" development to Isar scripts

hide Push

further simplifications of the integer development; converting more .ML files to Isar scripts

Tidying of the integer development; towards removing the abel_cancel simproc

Simplification of the development of Integers

More re-organising of numerical theorems

conversion of some Real theories to Isar scripts

Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs.

More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.

conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field

HOL: installation of Ring_and_Field as the basis for Naturals and Reals

conversion of Integ/Int_lemmas.ML to Isar script

including 0 ~= 1 in definition of Field

additions to Ring_and_Field

fixed a comment

new theorems for Rings

conversion of ML to Isar scripts

Improved error handling: add_primrec now prints out ill-formed equation in case of parse errors.

Type inference bug in Isar attributes "where" and "of" fixed.

tidied

Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.

Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.

fixed

set isatool usedir to verbose by default

Got rid of the structure "Int", which was obsolete and which obscured the eponymous Basis Library structure

Inserted additional checks in functions dest_prem and add_prod_factors, to allow side conditions of the form "x : S", where S is not an inductive set.

tidying

Tuned proof of choice_eq.

*** empty log message ***

added sydney unsw mirror. contact: me (gerwin.klein@nicta.com.au)

auto update

InductiveInvariant_examples illustrates advanced recursive function definitions

recursion

Added access to the mk_rews field (and friends).

Prevent recdef from looping when the inductio rule is simplified

improved tracing

partial conversion to Isar scripts

improved presentation

line-breaks; rewording

partial conversion to Isar scripts

Fixed bug in mk_ind_def that caused the inductive definition package to crash in cases where the declaration of a constant and its definition were located in different theory files.

use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)

allow \<^sub> in identifiers

included \<^sub> in the range of identifier chars

Fixed spelling error.

Added overview page.

Munich webserver is now atbroy1

trivial

finalconsts

Made judgments automatically declared final.

better presentation

Added info on the new 'finalconsts' command.

Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).

Added axiomatic specifications (ax_specification).

now accepts DOS and Mac line breaks

Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy

added a comment

removal of junk and improvement of the document

Fixed inefficiency in post_definition by adding weak case congruence rules to simpset.

Removed garbage accidentally left behind in file.

Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".

Improvements to Isar/Locales: premises generated by "includes" elements changed.

Changed order of prems in finprod_cong. Slight speedup.

Improvements wrt rule_tac.

Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".

new reference

tweak

misc tidying

Conversion of all main protocols from "Shared" to "Public". Removal of Key_supply_ax: modifications to possibility theorems. Improved presentation.

Tidying of SET's "possibility theorems" (removal of Key_supply_ax)

new example for the Isar version of the ZF manual

Fixed soundness bug.

conversion of NSP_Bad to Isar script

case_tac tweak

some basic new lemmas

Removal of the Key_supply axiom (affects many possbility proofs) and minor changes

new session HOL-SET-Protocol

Modified merge_aux to prevent newer names from getting overwritten by older names.

add_attribute now takes parser as argument.

Added "del" attribute for deleting equations.

Changed interface of add_attribute.

Improved efficiency of code generated for functions int and nat.

Improved efficiency of code generated for + and -

Improved efficiency of code generated for < predicate on natural numbers.

Mod due to new thm in Map.

Fixed blunder in the setup of the classical reasoner wrt. the constant "curry".

Added the constant "curry".

*** empty log message ***

Added new theorems

Added a number of thms about map restriction.

Tried to make parser a bit more standard-conforming.

Changed no_vars such that it outputs list of illegal schematic variables.

quantifier symbols

conversion of HOL/Auth/KerberosIV to new-style theory

new, separate specifications

Introduced new syntax for maplets x |-> y

Corrections due to John Matthews

Makes interactive proof scripting recognize the show_all_types flag.

Added 'ambiguity_is_error' flag, which, if set, makes the parser fail, rather than just issue a warning, when the input parsed is ambiguous.

Added show_all_types flag, such that all type information in the term is made explicit.

Method rule_tac understands Isar contexts: documentation.

Methods rule_tac etc support static (Isar) contexts.

Removed the extended digits again.

Fixed typos.

Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.

Added skalberg to recepients, changed admin from kleing to berghofe.

Converted to new style theories.

Prepared for extended identifiers (\<alpha>, etc.)

Improved the error messages (slightly).

Cleaned up the code.

New specification syntax added (the specification may be split over several properties).

Allowed for splitting the specification over several lemmas.

Improved handling of modes for equality predicate, to avoid ill-typed ML code due to comparisons between elements of function types.

Fixed problem with "code ind" attribute that caused code generator to fail for mutually recursive predicates.

Added function strong_conn for computing the strongly connected components of the graph.

Change from "tracing" to "warning", as requested by David Aspinall

final tweaks for Isar version

finished conversion to Isar format

new example

new case_tac method

partial conversion to Isar format

partial conversion to Isar format

new case_tac

For the Isar version of the ZF logics manual

converting ex/If to Isar script

A document for UNITY

reformatting change and mention of Introduction to Isabelle

corrections by Viktor Kuncak and minor updating

added tutorial

possibility proof!

ZhouGollmann: new example (fair non-repudiation protocol)

added lemma c_hupd_fst

Modifications after changes in MicroJava/J

Changed lemmas .._type_sound

Added lemma exec_no_xcpt

test_term now renames variable for size of test data to avoid clashes with variables already present in the term to be tested.

cleaned up

*** empty log message ***

Removed extraneous rev in function goal_params (the list of parameters is already reversed by rename_wrt_term).

opened new section for next Isabelle release

test_term now handles Match exception raised in generated code.

Replaced \<leadsto> by \<rightharpoonup>

Simplified a proof using presburger

new theory Library/NatPair

declarations moved from PreList.thy

Fixed two bugs: - presburger_tac now calls ObjectLogic.atomize_tac first to avoid failure when premises contain meta-level quantifiers or implications - The preprocessor now also filters out premises containing variables that are not of type int or nat.

Exported function get_mode.

header comment

new theory NatPair of the injection from nat*nat -> nat

Tidying and replacement of some axioms by specifications

tidied

Added some regression testing for simprocs

fixed simprocs

Added handling of meta implication and meta quantification.

Added handling of free variables (provided they are of sort HOL.type).

Tidied some examples

Added the specification command.

Changed bstring argument to xstring.

*** empty log message ***

Added optional theorem names for the constant definitions added during specification.

Added package for definition by specification.