converted Relation_Power to new-style theory

new and stronger lemmas and improved simplification for finite sets

tidied; removed references to HOL theories

added find_rewrites

*** empty log message ***

added find_rewrites

removal of NatArith.ML and Product_Type.ML

Fix pgmlsymbolson/off.

REorganized Finite_Set

Support PGIP <whitespace>, <dostep>, <doitem> elements as input

Insert pgmltext element into responses in PGIP mode

Added term cache to function condrew in order to speed up rewriting.

- Exported functions new_name and new_names - Fixed incompatible signatures problem in unfold_attr

Fixed bug in mk_gen_of_def that could cause non-termination of the generator for datatypes with nested recursion (such as trie).

Preprocessors now transfer theorems to current theory in order to avoid "incompatible signatures" exception.

Moved code generator setup for product type to Product_Type.thy

New code generator for let and split.

Realizer for exE now uses let instead of case.

First step in reorganizing Finite_Set

converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global

Comments and other tweaks by Jia

*** empty log message ***

converted Datatype_Universe to new-style theory

fixed bug in find functions that I introduced some time ago.

converted Lfp to new-style theory

improvements by Larry and Micheal Wahler

renamed attributes to lower case

made proofs more robust

all theories must be related to Reconstruction

converted Gfp to new-style theory

proof of subst by S Merz

comment added

link to tar.gz

proof of subst by S Merz

Started to clean up and generalize FiniteSet

add latex sugar

moved to Sugar

fixed typos

ignore generated

fixes to clause conversion

trying to fix the transfer problem

tidied

tuned

fixed typo

more sugar

clauses counted from 0

*** empty log message ***

Fixed print translation for ALL x > y etc

added ALL print-translation for > and >=.

*** empty log message ***

Added "ALL x > y" and relatives.

new CLAUSIFY attribute for proof reconstruction with lemmas

*** empty log message ***

antiquotations lhs and rhs

*** empty log message ***

Removed postfix >= because of new >= sugar

Added > and >= sugar

>= became > = because of new >=

fixed presentation

resolution package tools by Jia Meng

new antiquotations @{lhs thm} and @{rhs thm}

added antiquotations @{lhs thm} and @{rhs thm}

fixed another _

resolution package tools by Jia Meng

converted Wellfounded_Relations to Isar script

even more mboxes

Rule: put \mbox around premises/conclusion to avoid problems with super/sub-scripts.

blast_tac -> blast in comment (fix latex error)

*** empty log message ***

converted to Isar script, simplifying some results

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