obselete

onsolete

obsolete

New

render \<circ> as o not &circ; (which is ^)

minor code refactoring (typ_of_dtyp, size_of_dtyp)

exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)

comments edited

added ZCHAFF_VERSION

added ZCHAFF_VERSION

ML

Removed a "Matches are not exhaustive" warning

mod because of change in finite set induction

changed the order of !!-quantifiers in finite set induction. In Isar you can now write (insert x F) rather than the counterintuitive (insert F x).

Made test_term escape special characters in strings that caused the ML compiler to fail.

Functions nat_to_bv and bv_to_nat now really operate on natural numbers.

Added EfficientNat

Code generator plug-in for implementing natural numbers by integers.

Added Library/EfficientNat

Reimplemented some operations on "code lemma" table to avoid that code lemmas get lost during merge.

New theorem zpower_int

*** empty log message ***

prettier proof of setsum_diff

HTML conformity

renamed 1 lemmas

renamed 2 lemmas

relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring

external solvers may now overwrite existing temporary files

added lemma

Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff

*** empty log message ***

generalized lemma

added lemma

indentation

fixed proof

added lemmas

Added more lemmas

added lemmas

Restructured List and added "rotate"

comment modified

moved and renamed Integ/Equiv.thy

solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)

Barith removed VS: ----------------------------------------------------------------------

imports (new syntax for theory headers)

Tuned.

replace strangely encode space characters by &nbsp;

replaced strangely encoded space characters by &nbsp;

removed explicit mentioning of zChaffs version number

minor changes (comments/code refactoring)

removed Exercises document (available on separate web site now)

removed exercised document

Markup obtain as introducing a nested goal.

removed a "clone" (duplicate code)

minor rewording

Add <undoitem> for theory-state undos.

Renamed some variables to eliminate conflicts with constants. Introduced some abbreviations (following TPTP axiom sets) to reduce the amount of repetition. Uncommented some examples, which increases the runtime somewhat.

*** empty log message ***

DOCTYPE declaration added

Exercises added

More lemmas

minor code refactoring

improved "subscribe" link

added DOCTYPE and Content-Type declarations to make this a valid HTML file

isatool usedir -f

updated subscription wording and link

increased tracing and search bounds

tidied comments

* extended interface of record_split_simp_tac and record_split_simproc * improved record_type_abbr_tr'

user-interface impoved

fixed some awkward problems with nat/int simprocs

fixed reference to renamed theorem

isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)

Make <undostep> call undos_proof to display resulting proofstate.

efficienty improvement Heuristic is now the same as for the proof-generating alg.

Revert change to pgml_sym

Added type constraint to make SML/NJ happy.

Changed function cabs to also allow abstraction over Vars.

Added function merge_alists'.

Added function strip_type (for ctyps).

Added preprocessors.

Added setup for code generator.

Added simple code generator.

Removed code generator stuff. Code generation is now handled by code generator in typedef_package.

Added call to Codegen.preprocess.

Fixed problem with sorts in function make_casedists.

fixed urls

Simplification to symbol processing; put quotes around theory name in message.

Fix <closetheory>

Replaced PolyML specific print function by Display.print_thm(s)

converted some induct_tac to induct

added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.

Replaced list of bound variables in simpset by maximal index of bound variables. This allows new variable names to be generated more quickly (without calling variant).

record_split_simp_tac now can get simp rules as parameter

update

added and renamed

Added a few lemmas

mod becuase of chnage in induct

Added solution to exercise.

*** empty log message ***

tweaks concerned with poly bug-fixing

Replaced the_context() by theory "Presburger" in call of invoke_oracle.

Tuned some proofs.

Added entry in Settings menu for Toplevel.skip_proofs flag.

Some changes to allow skipping of proof scripts.

Proofs needed to be updated because induction now preserves name of induction variable.

Induction now preserves the name of the induction variable.

simplification tweaks for better arithmetic reasoning

*** empty log message ***

a very simple decision procedure for a fragment of bounded arithmetic

changed in order to insert Barith.thy

auto update

new simprules for abs and for things like a/b<1

revised simprules for division

PDF_VIEWER suggestion

Abstract for the Isabelle system

Add openblock/closeblock to other opengoal/closegoal elements

Allow scanning to recover and reconstruct bad input

patch to "display"

display-drafts now uses pdf!

tweaking of arithmetic proofs

Comments

tidied

display pdf as well as dvi

bug-fix with new records

Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.

tuned performance of record definition

tidying up; identifying the main theorems

Changes in "includes".

Bug fixes.

Add text_charref to encode a string using character references

Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>

Fix to unparse to not double-escape backslash

Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult

Add newline after CDATA for sake of HaXml

Modified locales: improved implementation of "includes".

some x-symbols

- Inserted additional check for equality types in check_mode_clause that avoids ill-typed code to be generated. - Mode inference algorithm now outputs additional diagnostic messages.

bug-fix

converting UNITY/MultisetSum.ML to Isar script

converted ZF/Induct/Multiset to Isar script

*** empty log message ***

undoing previous change

antisymmetry simproc

Added antisymmetry simproc

IntInf.divMod replaced by IntInf.div, IntInt.mod

new forward deduction capability for simplifier

new hooks for resolution by Jia Meng

Fix for schema changes in pgiptype

Tweak parentnames attribute on opentheory

Support parsing of -- {* comments *}. Add extra output channels.

Add info and debug output channels.

Adapted FloatArith.ML to SMLNJ 10.0.7

integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy

added check against indirect recursion

fixed discrete field.

tuned "discrete" field

made mult_mono_thms generic.

now rejects degenerate (looping) cases

new "respects" syntax for the congruent operator

*** empty log message ***

float2real is now globally available

Matrix theory

Matrix theory, linear programming

new theorem symD

listrel operator for lifting relations to lists

Fix file:/// and file://localhost/ to give absolute paths

Fix file:/// and file://localhost/ to return local file result

Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.

new example of a quotiented nested data type

added code to make use of case splitting to prove the specification equations for recursive definitions.

fixed presentation

new "respects" syntax for quotienting

new functions for sets of lists

reference to cla.ML replaced by Classical.thy

commentar eliminated a line 156 - arith raised Match exception at m dvd 2

corrected

m dvd t where m is non numeral is now catched!

Provers/blast.ML: depth_limit

depth limit (previously hard-coded with a value of 20) made a reference

comment modified

changes

begin_theory now takes optional path (current directory) as argument. This is needed for locating *.ML files connected with theories.

Fixed several bugs related to path specifications in theory names.

Function check_file now takes optional path (current directory) as an argument.

Adapted to new interface of function ThyLoad.check_file

Added function for "normalizing" absolute paths (i.e. dereferencing of symbolic links; the functions in path.ML cannot do this). This is used by function full_path.

new isatool dimacs2hol

initial version

new examples

proof reconstruction for external ATPs

fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon

new import syntax

*** empty log message ***

Add systemcmd.

Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.

Version for PGIP 2.X, with greatly improved parsing and XML handling.

Remove isar_readstring. Split read into scanner and parser.

Make token an eqtype to assist reconstructing input

Add scan_comment_whspc to skip space and comments in PGIP stream

import -> imports

import -> imports

todo before next release

improved wording course material

include course material page

Adapted text to new theory header syntax.

Added "import" and "begin"

Experimental version supporting PGIP, merged with main branch with help from Makarius.

Experimental pgip_isar.xml file

new theory header syntax.

New theory header syntax.

*** empty log message ***

Replaced `div and `mod in consts_code section by div and mod.

bugfix in read_dimacs_cnf_file

Disallowed "includes" in locale declarations.

Fixed bug in compile_clause that caused equality constraints to be "forgotten".

warning for recursion over IDTs added

Aded a thm.

*** empty log message ***

proof_of_evalc corrected;

Initial changes to extend arithmetic from individual types to type classes.

undid UN/INT syntax

undid UN/INT xsymbol syntax with subscripts.

make_clauses now meta

RS -> THEN

modified resolution proof

Undid \Union syntax with subscripts.

an updated treatment of the simprules

some structured proofs

added a thm

added some inj_on thms

Added a number of new thms and the new function remove1

proof mod

added a few thms

oracle corrected

aded comment

fixed tex problem

Typo.

New transitivity reasoners for transitivity only and quasi orders.

new simprules Int_subset_iff and Un_subset_iff

zdiv_int, zmod_int

conversion of Hyperreal/Filter to Isar scripts

Some comments added.

Documentation added/improved.

Modifications for trancl_tac (new solver in simplifier).

Documentation added; minor improvements.

Theories now take advantage of recent syntax improvements with (structure).

conversion of Hyperreal/{Fact,Filter} to Isar scripts

conversion of Integration and NSPrimes to Isar scripts

keep type_solver;

tuned dependencies;

added context type solver;

ZF/Simplifier: second copy of context type solver;

tuned output;

- optimized nodup_vars check in capply - new function dest_ctyp

removal of more iff-rules from RealDef.thy

removed some [iff] declarations from RealDef.thy, concerning inequalities

tidied

documents for ZF-AC and ZF-Constructible

conversion of SEQ.ML to Isar script

abs notation

fixed precedences

conversion of Hyperreal/MacLaurin_lemmas to Isar script

*** empty log message ***

converting Hyperreal/Transcendental to Isar script

New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver

minor formatting fixes

Modified \<Sum> syntax a little.

*** empty log message ***

new material courtesy of Norbert Voelker

updated;

Fixed latex problem

ring_1 -> ring

minor tweaks to go with the new version of the Accountability paper

removed some obsolete proofs

two new results

Some changes to allow qualified theory import.

- Moved code generator setup for lists from Main.thy to List.thy - Code generator now represents char type as strings of length 1 (easier to handle than encoding using nibbles)

Moved code generator setup for lists to List.thy

Added function dest_list.

Added simple check that allows code generator to produce code containing fewer redundant matches.

Added function unprefix.

tuned

added: get_extT_fields and get_recT_fields

added Complex/root

Fine-tuned sum syntax.

Corrected TeX problem.

Created.

Corrected TeX problems.

Added nice latex syntax.

int_ord = Int.compare, string_ord = String.compare;

*** empty log message ***

more summation syntax

more syntax

redefining sumr to be a translation to setsum

*** empty log message ***

Moved to new m<..<n syntax for set intervals.

*** empty log message ***

?

added {0::nat..n(} = {..n(}

Got rid of Summation and made it a translation into setsum instead.

read_dimacs_cnf_file added

added README

corrected bibtex entry

*** empty log message ***

context dependent components;

added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;

improved print_ss; tuned;

Simplifier and Classical Reasoner now support proof context dependent plug-ins;

local_cla/simpset_of;

- Added support for conditional equations whose premises involve inductive sets (useful in connection with THE operator) - Inductive and non-inductive sets (implemented as lists) can now be mixed

- Expressed infer_derivs' in terms of infer_deriv - Eta-expanded function instantiate to delay evaluation (avoids inefficiencies when proof terms are switched off)

- Removed obsolete clause in function check_str - test_term now temporarily sets print_mode to [] as well

new profiling function

adapted type of simprocs;

make SML/NJ happy;

added add_term_varnames, term_varnames;

got rid of obsolete meta_simpset; tuned;

major cleanup; got rid of obsolete meta_simpset;

tuned simprocs;

got rid of obsolete meta_simpset;

tuned;

removed obsolete dependency;

* Pure/Namespace: flag unique_names added * Pure/Tactic: print_tac outputs goal through trace channel * HOL/Simplifier: extended record_upd_simproc

print_tac now outputs goals through trace-channel

added flag unique_names

* record_upd_simproc also simplifies trivial updates: r(|x := x r|) = r * tuned quick and dirty mode

Added delete operation.

new treatment of binary numerals

Added reference record_definition_quick_and_dirty_sensitive, to skip proofs triggered by a record definition, if quick_and_dirty is enabled.

Made simplification procedures simpset-aware.

license change to BSD

support for sparse matrices

new method for explicit classical resolution

auto update

Merging the meta-simplifier with the Provers-simplifier. Next step: make the simplification procedure simpset-aware.

Norbert Voelker

ringpower to recpower

replaced monomorphic abs definitions by abs_if

tidied

Moved conversion rules from MetaSimplifier to Drule. refl_implies removed from Drule, instead imp_cong' exported from there.

tuned;

faster conversion into DIMACS CNF and DIMACS SAT format

tuned;

tuned;

improved print_theory;

added output, removed pp_undef;

added chars_only, symbol_output;

tuned certify_typ/term;

tuned output;

added unparse;

pretty_abbr;

tuned certify_typ;

Type.cert_typ;

tuned certify_term;

added certify_class/sort;

added >>> : transition list -> unit;

immediate_output;

avoid \...\;

File.quote_sysify_path;

Merged in license change from Isabelle2004

got rid of Output.output for default print mode;

added checkTimer;

added accumulated timing;

added escape, export encode_raw, default mode now trivial, tuned;

use_output: Symbol.escape;

tuned pp;

avoid premature evaluation of syn_of (wastes time in conjunction with pp);

Symbol.encode_raw;

tuned;

improved comments -- required by 'isatool latex -o syms';

more generous treatment of packages in draft prints;

scalable string_of_tree; tuned;

tuned exists_string;

isatool_document: verbose option;

Add \usepackage{latexsym}

new SAT solver interface

improved defcnf conversion

removal of magmas and semigroups

fixed 'requires' comments, which are needed for printing of drafts;

isub/isup quasi letter (again); tuned;

tuned;

tuned

isatool_document: writeln output;

tuned document;

prevent looping of error messages involving malformed symbols;

tuned;

removed unused help function;

new fib example

removal of x-symbol syntax <Sigma> for dependent products

ISABELLE_TMP

path instead of string;

added path;

tuned lexical syntax;

num tokens;

fixed bad link

slight speed improvement

strengthened some theorems

Jerusat settings added

entries for ZChaff and BerkMin added/modified

Oracle corrected

Further development of matrix theory

faster defcnf conversion

updated;

updated;

tuned;

tuned Present.drafts;

added display_drafts and print_drafts commands;

added PRINT_COMMAND setting

added isatool display and isatool print;

print document

display document (in DVI format)

root for draft documents;

Library.translate_string;

added trace (inefficient for very long input);

added translate_string;

added read (provides transition names and sources);

added output_known_symbols; tuned;

added name_of, source_of, source;

added Present.drafts;

added option 'isatool latex -o syms';

An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.

tuned;

improved RemoteFile;

tuned;

Removed this: not really ready yet.

Interface configuration for Isar

Sign.is_logtype;

prs: Output.output;

added split_ext; removed drop_ext;

tuned comment;

Scan.this_string;

tuned representation; added RemoteFile;

tuned;

added this_string;

tuned messages;

added is_logtype (replaces logtypes field of syntax); tuned merge;

removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode;

removed separate logtypes field of syntax;

Path.split_ext; more robust inform_file_processed;

Sign.is_logtype;

Syntax.default_mode;

added option 'locale=NAME';

Url.File;

* Document preparation: antiquotations provide option 'locale=NAME';

tuned comment;

updated/tuned identifier syntax;

updated notes on sub-/superscripts;

removed Syntax.test_read;

added a lemma lfp_ordinal_induct

fixed the groupI ambiguity

fixed the skolemize method

moved some cardinality results into main HOL

add_dummies no longer uses transform_error but handles specific exception Datatype_Empty instead.

Added exception Datatype_Empty.

mk_id is now also applied to identifiers in test_term.

Groups, Rings and supporting lemmas in ZF

Groups, Rings and supporting lemmas

Groups, Rings and supporting lemmas

avoid Args.list (lost update?);

added has_mode; handle_error: output raw;

Symbol.output;

no token translation / setup for Latex;

HOL: symbolic syntax of Eps;

More readable code.

pretty_thm/goals_aux, pretty_flexpair: pp;

avoid implicit arguments via refs;

Symbol.decode;

added datatype sym, val decode: symbol -> sym;

improved symbolic syntax of Eps: \<some> for mode "epsilon";

removed mlworks and smlnj-0.93 (obsolete);

tuned comments;

moved exception handling back to library.ML;

tuned exeption handling (capture/release);

removed Pure/ML-Systems/mlworks.ML Pure/ML-Systems/polyml-3.x.ML Pure/ML-Systems/smlnj-0.93.ML; added ML-Systems/polyml-time-limit.ML;

obsolete;

Tuned parse_att.

new rules for simplifying quantifiers with Sigma

Add alternative syntax for attributes

Add panic function which exits Isabelle immediately.

Removed ~10000 hack in function idx that can lead to inconsistencies when unifying terms with a large number of abstractions.