isabelle: Graph

isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
2004-10-28, by webertj
Make <undostep> call undos_proof to display resulting proofstate.
2004-10-28, by aspinall
efficienty improvement
2004-10-28, by chaieb
Revert change to pgml_sym
2004-10-27, by aspinall
Added type constraint to make SML/NJ happy.
2004-10-27, by berghofe
Changed function cabs to also allow abstraction over Vars.
2004-10-26, by berghofe
Added function merge_alists'.
2004-10-26, by berghofe
Added function strip_type (for ctyps).
2004-10-26, by berghofe
Added preprocessors.
2004-10-26, by berghofe
Added setup for code generator.
2004-10-26, by berghofe
Added simple code generator.
2004-10-26, by berghofe
Removed code generator stuff. Code generation is now handled by code
2004-10-26, by berghofe
Added call to Codegen.preprocess.
2004-10-26, by berghofe
Fixed problem with sorts in function make_casedists.
2004-10-26, by berghofe
fixed urls
2004-10-25, by nipkow
Simplification to symbol processing; put quotes around theory name in message.
2004-10-24, by aspinall
Fix <closetheory>
2004-10-21, by aspinall
Replaced PolyML specific print function by Display.print_thm(s)
2004-10-19, by berghofe
converted some induct_tac to induct
2004-10-19, by paulson
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.
2004-10-18, by dixon
Replaced list of bound variables in simpset by maximal index of bound
2004-10-18, by berghofe
record_split_simp_tac now can get simp rules as parameter
2004-10-15, by schirmer
update
2004-10-15, by nipkow
added and renamed
2004-10-15, by nipkow
Added a few lemmas
2004-10-14, by nipkow
mod becuase of chnage in induct
2004-10-13, by nipkow
Added solution to exercise.
2004-10-12, by nipkow
*** empty log message ***
2004-10-12, by nipkow
tweaks concerned with poly bug-fixing
2004-10-12, by paulson
Replaced the_context() by theory "Presburger" in call of invoke_oracle.
2004-10-11, by berghofe
Tuned some proofs.
2004-10-11, by berghofe
Added entry in Settings menu for Toplevel.skip_proofs flag.
2004-10-11, by berghofe
Some changes to allow skipping of proof scripts.
2004-10-11, by berghofe
Proofs needed to be updated because induction now preserves name of
2004-10-11, by nipkow
Induction now preserves the name of the induction variable.
2004-10-11, by nipkow
simplification tweaks for better arithmetic reasoning
2004-10-07, by paulson
*** empty log message ***
2004-10-06, by chaieb
a very simple decision procedure for a fragment of bounded arithmetic
2004-10-06, by chaieb
changed in order to insert Barith.thy
2004-10-06, by chaieb
auto update
2004-10-05, by paulson
new simprules for abs and for things like a/b<1
2004-10-05, by paulson
revised simprules for division
2004-10-04, by paulson
PDF_VIEWER suggestion
2004-10-04, by paulson
Abstract for the Isabelle system
2004-10-04, by paulson
Add openblock/closeblock to other opengoal/closegoal elements
2004-10-02, by aspinall
Allow scanning to recover and reconstruct bad input
2004-10-01, by aspinall
patch to "display"
2004-10-01, by paulson
display-drafts now uses pdf!
2004-10-01, by paulson
tweaking of arithmetic proofs
2004-10-01, by paulson
Comments
2004-10-01, by aspinall
tidied
2004-09-30, by paulson
display pdf as well as dvi
2004-09-30, by kleing
bug-fix with new records
2004-09-30, by schirmer
Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.
2004-09-29, by aspinall
tuned performance of record definition
2004-09-29, by schirmer
tidying up; identifying the main theorems
2004-09-29, by paulson
Changes in "includes".
2004-09-28, by ballarin
Bug fixes.
2004-09-28, by ballarin
Add text_charref to encode a string using character references
2004-09-28, by aspinall
Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
2004-09-28, by aspinall
Fix to unparse to not double-escape backslash
2004-09-28, by aspinall
Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
2004-09-27, by aspinall
Add newline after CDATA for sake of HaXml
2004-09-27, by aspinall
Modified locales: improved implementation of "includes".
2004-09-27, by ballarin
some x-symbols
2004-09-23, by paulson
- Inserted additional check for equality types in check_mode_clause that
2004-09-23, by berghofe
bug-fix
2004-09-22, by schirmer
converting UNITY/MultisetSum.ML to Isar script
2004-09-19, by paulson
converted ZF/Induct/Multiset to Isar script
2004-09-17, by paulson
*** empty log message ***
2004-09-13, by nipkow
undoing previous change
2004-09-11, by nipkow
antisymmetry simproc
2004-09-11, by nipkow
Added antisymmetry simproc
2004-09-10, by nipkow
IntInf.divMod replaced by IntInf.div, IntInt.mod
2004-09-10, by obua
new forward deduction capability for simplifier
2004-09-10, by nipkow
new hooks for resolution by Jia Meng
2004-09-09, by paulson
Fix for schema changes in pgiptype
2004-09-09, by aspinall
Tweak parentnames attribute on opentheory
2004-09-08, by aspinall
Support parsing of -- {* comments *}. Add extra output channels.
2004-09-08, by aspinall
Add info and debug output channels.
2004-09-08, by aspinall
Adapted FloatArith.ML to SMLNJ 10.0.7
2004-09-08, by obua
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
2004-09-07, by oheimb
added check against indirect recursion
2004-09-07, by oheimb
fixed discrete field.
2004-09-07, by nipkow
tuned "discrete" field
2004-09-07, by nipkow
made mult_mono_thms generic.
2004-09-06, by nipkow
now rejects degenerate (looping) cases
2004-09-06, by paulson
new "respects" syntax for the congruent operator
2004-09-06, by paulson
*** empty log message ***
2004-09-03, by nipkow
float2real is now globally available
2004-09-03, by obua
Matrix theory
2004-09-03, by obua
Matrix theory, linear programming
2004-09-03, by obua
new theorem symD
2004-09-03, by paulson
listrel operator for lifting relations to lists
2004-09-03, by paulson
Fix file:/// and file://localhost/ to give absolute paths
2004-09-03, by aspinall
Fix file:/// and file://localhost/ to return local file result
2004-09-03, by aspinall
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
2004-09-03, by aspinall
new example of a quotiented nested data type
2004-09-02, by paulson
added code to make use of case splitting to prove the specification equations for recursive definitions.
2004-09-02, by dixon
fixed presentation
2004-09-02, by paulson
new "respects" syntax for quotienting
2004-09-01, by paulson
new functions for sets of lists
2004-09-01, by paulson
reference to cla.ML replaced by Classical.thy
2004-08-30, by webertj
commentar eliminated a line 156 - arith raised Match exception at m dvd 2
2004-08-30, by chaieb
corrected
2004-08-30, by chaieb
m dvd t where m is non numeral is now catched!
2004-08-30, by chaieb
Provers/blast.ML: depth_limit
2004-08-29, by webertj
depth limit (previously hard-coded with a value of 20) made a reference
2004-08-29, by webertj
comment modified
2004-08-26, by webertj
changes
2004-08-24, by obua
begin_theory now takes optional path (current directory) as argument.
2004-08-23, by berghofe
Fixed several bugs related to path specifications in theory names.
2004-08-23, by berghofe
Function check_file now takes optional path (current directory) as an argument.
2004-08-23, by berghofe
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
Added function unprefix.
2004-07-19, by berghofe
tuned
2004-07-18, by schirmer
added: get_extT_fields and
2004-07-16, by schirmer
added Complex/root
2004-07-16, by nipkow
Fine-tuned sum syntax.
2004-07-16, by nipkow
Corrected TeX problem.
2004-07-16, by nipkow
Created.
2004-07-16, by nipkow
Corrected TeX problems.
2004-07-16, by nipkow
Added nice latex syntax.
2004-07-16, by nipkow
int_ord = Int.compare, string_ord = String.compare;
2004-07-16, by wenzelm
*** empty log message ***
2004-07-15, by nipkow
more summation syntax
2004-07-15, by nipkow
more syntax
2004-07-15, by nipkow
redefining sumr to be a translation to setsum
2004-07-15, by paulson
*** empty log message ***
2004-07-15, by nipkow
Moved to new m<..<n syntax for set intervals.
2004-07-15, by nipkow
*** empty log message ***
2004-07-15, by nipkow
?
2004-07-14, by nipkow
added {0::nat..n(} = {..n(}
2004-07-14, by nipkow
Got rid of Summation and made it a translation into setsum instead.
2004-07-13, by nipkow
read_dimacs_cnf_file added
2004-07-12, by webertj
added README
2004-07-12, by oheimb
corrected bibtex entry
2004-07-12, by oheimb
*** empty log message ***
2004-07-12, by nipkow
context dependent components;
2004-07-11, by wenzelm
added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;
2004-07-11, by wenzelm
improved print_ss; tuned;
2004-07-11, by wenzelm
Simplifier and Classical Reasoner now support proof context dependent plug-ins;
2004-07-11, by wenzelm
local_cla/simpset_of;
2004-07-11, by wenzelm
- Added support for conditional equations whose premises involve
2004-07-09, by berghofe
- Expressed infer_derivs' in terms of infer_deriv
2004-07-09, by berghofe