isabelle: Graph

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

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