isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip

Adapted to new interface of function ThyLoad.check_file
2004-08-23, by berghofe
Added function for "normalizing" absolute paths (i.e. dereferencing of
2004-08-23, by berghofe
new isatool dimacs2hol
2004-08-23, by webertj
initial version
2004-08-23, by webertj
new examples
2004-08-20, by paulson
proof reconstruction for external ATPs
2004-08-20, by paulson
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
2004-08-20, by paulson
new import syntax
2004-08-19, by nipkow
*** empty log message ***
2004-08-19, by nipkow
Add systemcmd.
2004-08-19, by aspinall
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
2004-08-19, by aspinall
Version for PGIP 2.X, with greatly improved parsing and XML handling.
2004-08-18, by aspinall
Remove isar_readstring. Split read into scanner and parser.
2004-08-18, by aspinall
Make token an eqtype to assist reconstructing input
2004-08-18, by aspinall
Add scan_comment_whspc to skip space and comments in PGIP stream
2004-08-18, by aspinall
import -> imports
2004-08-18, by nipkow
import -> imports
2004-08-18, by nipkow
todo before next release
2004-08-17, by kleing
improved wording course material
2004-08-17, by kleing
include course material page
2004-08-17, by kleing
Adapted text to new theory header syntax.
2004-08-16, by nipkow
Added "import" and "begin"
2004-08-16, by nipkow
Experimental version supporting PGIP, merged with main branch with help from Makarius.
2004-08-16, by aspinall
Experimental pgip_isar.xml file
2004-08-16, by aspinall
new theory header syntax.
2004-08-16, by nipkow
New theory header syntax.
2004-08-16, by nipkow
*** empty log message ***
2004-08-16, by nipkow
Replaced `div and `mod in consts_code section by div and mod.
2004-08-16, by berghofe
bugfix in read_dimacs_cnf_file
2004-08-14, by webertj
Disallowed "includes" in locale declarations.
2004-08-12, by ballarin
Fixed bug in compile_clause that caused equality constraints
2004-08-10, by berghofe
warning for recursion over IDTs added
2004-08-09, by webertj
Aded a thm.
2004-08-09, by nipkow
*** empty log message ***
2004-08-06, by chaieb
proof_of_evalc corrected;
2004-08-06, by chaieb
Initial changes to extend arithmetic from individual types to type classes.
2004-08-06, by nipkow
undid UN/INT syntax
2004-08-06, by nipkow
undid UN/INT xsymbol syntax with subscripts.
2004-08-06, by nipkow
make_clauses now meta
2004-08-06, by paulson
RS -> THEN
2004-08-06, by paulson
modified resolution proof
2004-08-06, by paulson
Undid \Union syntax with subscripts.
2004-08-06, by nipkow
an updated treatment of the simprules
2004-08-05, by paulson
some structured proofs
2004-08-05, by paulson
added a thm
2004-08-04, by nipkow
added some inj_on thms
2004-08-04, by nipkow
Added a number of new thms and the new function remove1
2004-08-04, by nipkow
proof mod
2004-08-04, by nipkow
added a few thms
2004-08-04, by nipkow
oracle corrected
2004-08-04, by chaieb
aded comment
2004-08-04, by nipkow
fixed tex problem
2004-08-04, by nipkow
Typo.
2004-08-03, by ballarin
New transitivity reasoners for transitivity only and quasi orders.
2004-08-03, by ballarin
new simprules Int_subset_iff and Un_subset_iff
2004-08-03, by paulson
zdiv_int, zmod_int
2004-08-02, by obua
conversion of Hyperreal/Filter to Isar scripts
2004-08-02, by paulson
Some comments added.
2004-08-02, by ballarin
Documentation added/improved.
2004-08-02, by ballarin
Modifications for trancl_tac (new solver in simplifier).
2004-08-02, by ballarin
Documentation added; minor improvements.
2004-08-02, by ballarin
Theories now take advantage of recent syntax improvements with (structure).
2004-08-02, by ballarin
conversion of Hyperreal/{Fact,Filter} to Isar scripts
2004-07-31, by paulson
conversion of Integration and NSPrimes to Isar scripts
2004-07-30, by paulson
keep type_solver;
2004-07-30, by wenzelm
tuned dependencies;
2004-07-30, by wenzelm
added context type solver;
2004-07-30, by wenzelm
ZF/Simplifier: second copy of context type solver;
2004-07-30, by wenzelm
tuned output;
2004-07-30, by wenzelm
- optimized nodup_vars check in capply
2004-07-29, by berghofe
removal of more iff-rules from RealDef.thy
2004-07-29, by paulson
removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-07-29, by paulson
tidied
2004-07-29, by paulson
documents for ZF-AC and ZF-Constructible
2004-07-29, by paulson
conversion of SEQ.ML to Isar script
2004-07-28, by paulson
abs notation
2004-07-28, by paulson
fixed precedences
2004-07-28, by paulson
conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-07-28, by paulson
*** empty log message ***
2004-07-27, by ballarin
converting Hyperreal/Transcendental to Isar script
2004-07-26, by paulson
New prover for transitive and reflexive-transitive closure of relations.
2004-07-26, by ballarin
minor formatting fixes
2004-07-22, by webertj
Modified \<Sum> syntax a little.
2004-07-22, by nipkow
*** empty log message ***
2004-07-22, by nipkow
new material courtesy of Norbert Voelker
2004-07-22, by paulson
updated;
2004-07-21, by wenzelm
Fixed latex problem
2004-07-21, by nipkow
ring_1 -> ring
2004-07-20, by nipkow
minor tweaks to go with the new version of the Accountability paper
2004-07-20, by paulson
removed some obsolete proofs
2004-07-20, by paulson
two new results
2004-07-20, by paulson
Some changes to allow qualified theory import.
2004-07-19, by berghofe
- Moved code generator setup for lists from Main.thy to List.thy
2004-07-19, by berghofe
Moved code generator setup for lists to List.thy
2004-07-19, by berghofe
Added function dest_list.
2004-07-19, by berghofe
Added simple check that allows code generator to produce code containing
2004-07-19, by berghofe

less more | (0) -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle