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

*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** empty log message ***
2005-04-13, by wenzelm
new signalling primmitives for sml/nj compatibility
2005-04-13, by paulson
*** empty log message ***
2005-04-12, by nipkow
tweaks mainly to achieve sml/nj compatibility
2005-04-12, by paulson
fixing an incompatibility with Posix.IO.mkTextReader
2005-04-12, by paulson
auto update
2005-04-11, by paulson
removal of Main and other tidying up
2005-04-11, by paulson
First release of interpretation commands.
2005-04-11, by ballarin
tuned
2005-04-11, by nipkow
added \restriction
2005-04-11, by nipkow
tuned Map, renamed lex stuff in List.
2005-04-11, by nipkow
Added lots of AMS harpoons
2005-04-10, by nipkow
_(_|_) is now override_on
2005-04-10, by nipkow
tuned
2005-04-10, by nipkow
section on qmark
2005-04-10, by nipkow
fixed the syntax of infix declarations
2005-04-09, by paulson
thmref: selection syntax;
2005-04-09, by wenzelm
update syntax of 'where' and 'of';
2005-04-09, by wenzelm
added PDF_VIEWER, ISABELLE_DOC_FORMAT;
2005-04-09, by wenzelm
Reconstruction code, now packaged to avoid name clashes
2005-04-08, by paulson
temporarily removed ATP code
2005-04-08, by paulson
removed bad code
2005-04-07, by paulson
Changed prob1.dfg to prob_1.dfg
2005-04-07, by quigley
Got rid of Main.thy reference
2005-04-07, by quigley
Integrating the reconstruction files into the building of HOL
2005-04-07, by quigley
Reconstruction.thy and IsaMakefile updated
2005-04-07, by quigley
*** empty log message ***
2005-04-07, by nipkow
new meta-level rules
2005-04-07, by paulson
*** empty log message ***
2005-04-07, by nipkow
reverted renaming of Some/None in comments and strings;
2005-04-07, by wenzelm
added term_8;
2005-04-07, by wenzelm
added get_axiom_i, invoke_oracle_i;
2005-04-07, by wenzelm
Drule.add_used;
2005-04-07, by wenzelm
invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!
2005-04-07, by wenzelm
added add_used; include tpairs;
2005-04-07, by wenzelm
improved exn_message;
2005-04-07, by wenzelm
Thm.invoke_oracle_i;
2005-04-07, by wenzelm
Scan.peek;
2005-04-07, by wenzelm
tuned updates, added map_entry;
2005-04-07, by wenzelm
added some, peek, trace'; tuned;
2005-04-07, by wenzelm
added header;
2005-04-07, by wenzelm
improved comments;
2005-04-07, by wenzelm
reverted renaming of Some/None in comments and strings;
2005-04-07, by wenzelm
handle Option instead of OPTION;
2005-04-07, by wenzelm
updated it
2005-04-06, by nipkow
watcher.ML and watcher.sig changed. Debug files now write to tmp.
2005-04-06, by quigley
Current version of res_atp.ML - causes an error when I run it. C.Q.
2005-04-05, by quigley
lexicographic order by Norbert Voelker
2005-04-05, by paulson
arg_cong2 by Norbert Voelker
2005-04-05, by paulson
*** empty log message ***
2005-04-05, by nipkow
Updated to add watcher code.
2005-04-04, by quigley
CVSfj
2005-04-04, by quigley
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
2005-04-02, by huffman
converted to new-style theory
2005-04-02, by huffman
convert to new-style theory
2005-04-01, by huffman
x-symbols and other tidying
2005-04-01, by paulson
Updated import configuration.
2005-04-01, by skalberg
bring make to delete files on error
2005-04-01, by gagern
patch to get it working again
2005-04-01, by paulson
*** empty log message ***
2005-03-31, by quigley
*** empty log message ***
2005-03-31, by quigley
*** empty log message ***
2005-03-31, by quigley
added theorems eta_cfun and cont2cont_eta
2005-03-31, by huffman
chfin now a subclass of po, proved instance chfin < cpo
2005-03-31, by huffman
cleaned up some proofs
2005-03-31, by huffman
fixed bug in prj' function
2005-03-31, by huffman
changed comments to text blocks, cleaned up a few proofs
2005-03-31, by huffman
converted from DOS to UNIX format
2005-03-30, by paulson
converted HOL-Subst to tactic scripts
2005-03-29, by paulson
conversion of UNITY to Isar scripts
2005-03-28, by paulson
new display of theory stamps
2005-03-26, by paulson
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
2005-03-26, by gagern
use Library/Multiset instead of own definition
2005-03-26, by kleing
fixed typo (multiset_append)
2005-03-26, by kleing
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
2005-03-25, by aspinall
tidied up
2005-03-25, by paulson
Revert previous change (but leave comments).
2005-03-25, by aspinall
Support new PGIP commands redostep, redoitem
2005-03-25, by aspinall
Support non-standard file: URL syntax, temporarily.
2005-03-25, by aspinall
Further work on interpretation commands. New command `interpret' for
2005-03-24, by ballarin
*** empty log message ***
2005-03-24, by ballarin
Transitivity reasoner ignores types amenable to linear arithmetic.
2005-03-24, by ballarin
COMMENT IN WRONG PLACE
2005-03-24, by paulson
replaced bool by a new datatype "bit" for binary numerals
2005-03-23, by paulson
temporary removal of Import
2005-03-23, by paulson
tidied
2005-03-23, by paulson
auto update
2005-03-22, by paulson
deleted a pointless comment
2005-03-22, by paulson
ensuring that "equal" is not a function
2005-03-22, by paulson
auto update
2005-03-18, by paulson
meson now checks that problems are first-order
2005-03-17, by paulson
added string_of_term
2005-03-17, by nipkow
Bugfix related to the interpretation of IDT constructors
2005-03-17, by webertj
more concise ASCII escaping
2005-03-15, by paulson
fixed syntax for Let <x,y> = a in e
2005-03-14, by huffman
bug fixes involving typechecking clauses
2005-03-14, by paulson
removed theorems about Sinl_Rep and Sinr_Rep
2005-03-12, by huffman
simplified some definitions, many proofs are much shorter
2005-03-11, by huffman
minor Library.option related modifications
2005-03-11, by webertj
code reformatted
2005-03-11, by webertj
code reformatted
2005-03-11, by webertj
fixed bug: domain package can now define three or more mutually recursive types simultaneously
2005-03-11, by huffman
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
2005-03-11, by huffman
fixed filename in header
2005-03-10, by huffman