isabelle: Graph

Moved cterm_fun from Thm to Drule.
2005-04-21, by berghofe
Modified variable index in proof (necessary due to changes in the kernel).
2005-04-21, by berghofe
Adapted to new interface of instantiation and unification / matching functions.
2005-04-21, by berghofe
Made inst1_tac more robust against changes of variable indices.
2005-04-21, by berghofe
fix
2005-04-21, by nipkow
tuning locales
2005-04-21, by nipkow
removed tracing info
2005-04-21, by paulson
added hearder lines and deleted some redundant material
2005-04-21, by paulson
adding the Proof General preview
2005-04-21, by paulson
improved SML/NJ compatibility, etc.
2005-04-21, by paulson
Added op in front of constructor for better parsing.
2005-04-20, by gagern
Fix automatic determination of poly version.
2005-04-20, by gagern
removed redundant readlink call
2005-04-20, by gagern
call to Array.modifyi replaced
2005-04-20, by webertj
Corrected the problem with the ATP directory.
2005-04-20, by quigley
Used locale interpretations everywhere. -> lemma had new name
2005-04-20, by nipkow
Used locale interpretations everywhere.
2005-04-20, by nipkow
Removed remaining references to Main.thy in reconstruction code.
2005-04-20, by quigley
Allow symlinks to shell scripts
2005-04-20, by gagern
added locale instantiation
2005-04-20, by kleing
refute extended
2005-04-19, by webertj
syntax fix
2005-04-19, by paulson
more tidying of libraries in Reconstruction
2005-04-19, by paulson
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
2005-04-19, by quigley
auto update
2005-04-19, by paulson
restored the target HOL-Complex-Import
2005-04-19, by paulson
fixed presentation
2005-04-19, by paulson
Removed mult_commute axiom from comm_semiring axclass.
2005-04-19, by obua
compilation error fixed
2005-04-19, by webertj
support for recursion over mutually recursive IDTs
2005-04-18, by webertj
Cleaned up, now use interpretation.
2005-04-18, by ballarin
Cleaned up, now uses interpretation.
2005-04-18, by ballarin
deleted obsolete code
2005-04-18, by paulson
Interpretation supports statically scoped attributes; documentation.
2005-04-18, by ballarin
updated;
2005-04-17, by wenzelm
added delete_safe, insert, remove, remove_multi;
2005-04-17, by wenzelm
clarified insert/remove;
2005-04-17, by wenzelm
tuned;
2005-04-17, by wenzelm
binds/thms: do not store options, but delete from table;
2005-04-17, by wenzelm
tuned comments;
2005-04-17, by wenzelm
removed;
2005-04-17, by wenzelm
expect translations functions to be stamped already;
2005-04-16, by wenzelm
added stamp_trfun, mk_trfun, eq_trfun;
2005-04-16, by wenzelm
tuned extend_prtabs;
2005-04-16, by wenzelm
added make_gram;
2005-04-16, by wenzelm
identify binder translations only once (admits remove);
2005-04-16, by wenzelm
Syntax.mk_trfun;
2005-04-16, by wenzelm
tuned (t)inst_tab_elem;
2005-04-16, by wenzelm
added 'no_syntax' command;
2005-04-16, by wenzelm
added del_modesyntax(_i);
2005-04-16, by wenzelm
added del_modesyntax(_i);
2005-04-16, by wenzelm
added gen_remove, remove;
2005-04-16, by wenzelm
Pure: command 'no_syntax' removes grammar declarations;
2005-04-16, by wenzelm
removed;
2005-04-16, by wenzelm
speed improvements for the domain package
2005-04-16, by huffman
New file for theorems used by the domain package
2005-04-16, by huffman
rermoved pointless example
2005-04-15, by nipkow
yet more tidying up: removal of some references to Main
2005-04-15, by paulson
*** empty log message ***
2005-04-15, by nipkow
New
2005-04-15, by nipkow
more tidying up of the SPASS interface
2005-04-15, by paulson
Removed most of the atp interface from Pure.
2005-04-15, by ballarin
Include automatic determination of poly version.
2005-04-14, by aspinall
Add RDISTDIR option used by Isabelle RPM.
2005-04-14, by aspinall
Added thm names
2005-04-14, by nipkow
Removed dir Orderings in Library
2005-04-14, by nipkow
fix: added path to garbage
2005-04-14, by kleing
added LaTeXsugar
2005-04-14, by kleing
added Makefile and generated files to make document available for makedist
2005-04-14, by kleing
Locales: proper static binding of attribute syntax;
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
*** 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
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
2005-03-10, by huffman
Registrations of global locale interpretations: improved, better naming.
2005-03-10, by ballarin
Debugging code (error_depth) removed.
2005-03-10, by ballarin
First version of global registration command.
2005-03-09, by ballarin
fix integer overflow in numeral syntax for SML NJ.
2005-03-08, by obua
fixed variable name
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
removed Cprod3_lemma1 and Cprod3_lemma2
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
added subsection headings, cleaned up some proofs
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
added subsections and text for document generation
2005-03-07, by huffman
Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
2005-03-07, by huffman
HTML 4.01 Transitional conformity
2005-03-07, by webertj
refute_params: default value itself=1 added (for type classes)
2005-03-07, by webertj
HTML 4.01 Transitional conformity
2005-03-07, by webertj
HTML 4.01 Transitional conformity
2005-03-07, by webertj
now checks for higher-order vars
2005-03-07, by paulson
Cleaning up HOL/Matrix
2005-03-07, by obua
Tools/meson.ML: signature, structure and "open" rather than "local"
2005-03-07, by paulson
add header
2005-03-04, by huffman
fix headers
2005-03-04, by huffman
converted to new-style theories, and combined numbered files
2005-03-04, by huffman
document generation for HOLCF
2005-03-04, by huffman
Removed practically all references to Library.foldr.
2005-03-04, by skalberg
new first_order test
2005-03-04, by paulson
removed dead code
2005-03-04, by paulson
interpreter for Finite_Set.Finites added
2005-03-03, by webertj
Move towards standard functions.
2005-03-03, by skalberg
fixed proof
2005-03-03, by nipkow
converted to new-style theory
2005-03-03, by huffman
converted to new-style theory
2005-03-03, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
another reorganization of setsums and intervals
2005-03-02, by nipkow
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
2005-03-02, by dixon
obscured the e-mail address lcp@cl
2005-03-02, by paulson
new lemmas int_diff_cases
2005-03-02, by paulson
eliminated deps for removed files
2005-03-02, by huffman