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;