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