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.