replaced bool by a new datatype "bit" for binary numerals

temporary removal of Import

tidied

auto update

deleted a pointless comment

ensuring that "equal" is not a function

auto update

meson now checks that problems are first-order

added string_of_term

Bugfix related to the interpretation of IDT constructors

more concise ASCII escaping

fixed syntax for Let <x,y> = a in e

bug fixes involving typechecking clauses

removed theorems about Sinl_Rep and Sinr_Rep

simplified some definitions, many proofs are much shorter

minor Library.option related modifications

code reformatted

code reformatted

fixed bug: domain package can now define three or more mutually recursive types simultaneously

domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u

fixed filename in header

instance u :: (cpo) pcpo -- argument type no longer needs to be pointed

Registrations of global locale interpretations: improved, better naming.

Debugging code (error_depth) removed.

First version of global registration command.

fix integer overflow in numeral syntax for SML NJ.

fixed variable name

reordered and arranged for document generation, cleaned up some proofs

removed Cprod3_lemma1 and Cprod3_lemma2

reordered and arranged for document generation, cleaned up some proofs

added subsection headings, cleaned up some proofs

reordered and arranged for document generation, cleaned up some proofs

arranged for document generation, cleaned up some proofs

added subsections and text for document generation

Added dependency document/root.tex, and -g true option to isatool; document generation should work now.

HTML 4.01 Transitional conformity

refute_params: default value itself=1 added (for type classes)

HTML 4.01 Transitional conformity

HTML 4.01 Transitional conformity

now checks for higher-order vars

Cleaning up HOL/Matrix

Tools/meson.ML: signature, structure and "open" rather than "local"

add header

fix headers

converted to new-style theories, and combined numbered files

document generation for HOLCF

Removed practically all references to Library.foldr.

new first_order test

removed dead code

interpreter for Finite_Set.Finites added

Move towards standard functions.

fixed proof

converted to new-style theory

converted to new-style theory

converted to new-style theory

converted to new-style theory

converted to new-style theory

converted to new-style theory

converted to new-style theory

another reorganization of setsums and intervals

lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.

obscured the e-mail address lcp@cl

new lemmas int_diff_cases

eliminated deps for removed files

merged into Discrete.thy

converted to new-style theory

integrated Jeremy's FiniteLib

spider dogding

added setsum_diff1' which holds in more general cases than setsum_diff1

unfold theorems for trancl and rtrancl

lucas - added more comments and an extra type to clarify the code.

Modified node_trans to avoid duplication of signature stamps when undoing.

exception SAME removed

major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes

suminf -> \<Sum>

Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.

removed redundant lemmas and simprules

more setsum tuning

more fine tuniung

fixed proof

removed superfluous setsum_constant

comprehensive cleanup, replacing sumr by setsum

lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.

continued eliminating sumr

starting to get rid of sumr

tuning

*** empty log message ***

refine now provides specific cases "goal1" ... "goaln" for addressing subgoals of a proof state.

simplified a proof

Deleted Library.option type.

Fully qualified refl and trans to avoid confusion with theorems in Lattice_Locales.partial_order.

Optimized present_tokens to produce fewer newlines when hiding proofs.

New reference Toplevel.debug for verbose printing of exns.

update from Larry

some stuff is now redundant.

HOL.order -> Orderings.order due to restructering

Moved oderings from HOL into the new Orderings.thy

Added paper by M. Takahashi.

Added proof of eta-postponement theorem (using parallel eta-reduction).

non-inductive fold1Set proofs

simplified a key lemma for foldSet

Toplevel.debug for debugging in Isar.

Fixed bug in select_thm.

Subscripts for theorem lists now start at 1.

mention authors are acknowledged for isabelle-lemmas

more preview

pointer to isabelle-lemmas submission list

added lattice_locales

Extracted generic lattice stuff to new Lattice_Locales.thy

New

new foldSet proofs

revised fold1 proofs

revised fold1 proofs

cvs merge problem fixed

new treatment of fold1

Fixed lattice defns

*** empty log message ***

fixed latex problems by including bigsqcap

fixed latex problems

fixed mac line

Added Lattice locale

clausification and proof reconstruction

comment

Added semi-lattice locales and reorganized fold1 lemmas

added find_rewrites

new treatment of demodulation in proof reconstruction

don't generate latex for LaTeXsugar and OptionalSugar

removed sugar.sty (obsolete for devel version)

not needed any more by LaTeXSugar

Document now applies to devel version (and Isabelle 2005)

Replaced application of subst by simplesubst in proof of app_Var_NF to avoid problems with program extraction.

Replaced application of subst by simplesubst in proof of rev_induct to avoid problems with program extraction.

tidying of some subst/simplesubst proofs

generalization and tidying

improved handling of chained facts

Max_le -> Max_ge

fold and fol1 changes

added [simp]

link to PG FAQ for start up problem

the new subst tactic, by Lucas Dixon

renamed a few vars, added a lemma

proof simpification

moved sugar.sty to textinputs

-H false for showing proofs (not -H true)

fixed bugs

- Proofs are now hidden by default when generating documents - New syntax for referring to theorems in lists - Improvements to theory loader (relative and absolute paths)

Proofs are now hidden by default.

- Proofs are now hidden by default - Added show_var_qmarks flag

Added show_var_qmarks flag.

*** empty log message ***

added OptionalSugar

new

moved to HOL/Library

*** empty log message ***

implemented cache for conversion to clauses

enclosed in (*<*) (*>*)

Added variant of eres_inst_tac that operates on indexnames instead of strings.

Adapted to modified interface of PureThy.get_thm(s).

Eliminated hack for deleting leading question mark from induction variable name.

Replaced xstring by thmref.

Removed unnecessary subsignature checks to speed up rewriting.

Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.

Replaced xstring by thmref.

Adapted to modified interface of PureThy.get_thm(s).

Specific theorems in a named list of theorems can now be referred to via indices (type thmref).

updated description of arith_tac

thin_tac now works on P==>Q

some rationalizing of res_inst_tac

Jia Meng: delta simpsets and clasets

fixed thin_tac with higher-level assumptions by removing the old code to handle the iterated introduction of parameters

inserted quotes preparatory to conversion

fixed the treatment of demodulation and paramodulation

negate_nead (???) changed to negated_asm_of_head

new theorem image_eq_fold

auto update

*** empty log message ***

induct_tac and case_tac no longer depend on Syntax.string_of_vname.

indexname function now parses type variables as well; changed input type from string list to string.

Added variants of instantiation functions that operate on pairs of type (indexname * string) instead of (string * string).

*** empty log message ***

Removed div/mod ML code because it fails for 0.

made diff_less a simp rule

Added ChangeLog

Tuned.

Option for hiding proof scripts in documents.

Added -H option for hiding proof scripts and other commands.

Swapped session.ML and isar_output.ML

Added flag for hiding proofs in documents to use_dir.

Added table of commands to be hidden in LaTeX output.

excursion_result now also passes previous state to presentation functions. This is useful for hiding proof scripts.

Implemented hiding of proofs and other commands.

new citation

suggestions by Jeremy Siek

use ISO date format

added list_all_rev

[ .. (] -> [ ..< ]

*** empty log message ***

added simproc for Let

added print translation for split: split f --> %(x,y). f x y

Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for printing.

Isabelle 2005 - preview

sugar, not sugari. stupid vi ;-)

removed two looping simplifications in SetInterval.thy; deleted the .ML file

*** empty log message ***

Further fix to a bug (involving equational premises) in inductive definitions

fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions

LaTeXsugar

removal of archaic Abs/Rep proofs

*** empty log message ***

removal of HOL_Lemmas

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.