2005-04-07 paulson 2005-04-07 removed bad code
2005-04-07 quigley 2005-04-07 Changed prob1.dfg to prob_1.dfg
2005-04-07 quigley 2005-04-07 Got rid of Main.thy reference
2005-04-07 quigley 2005-04-07 Integrating the reconstruction files into the building of HOL
2005-04-07 quigley 2005-04-07 Reconstruction.thy and IsaMakefile updated
2005-04-07 nipkow 2005-04-07 *** empty log message ***
2005-04-07 paulson 2005-04-07 new meta-level rules
2005-04-07 nipkow 2005-04-07 *** empty log message ***
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-04-07 wenzelm 2005-04-07 added term_8;
2005-04-07 wenzelm 2005-04-07 added get_axiom_i, invoke_oracle_i;
2005-04-07 wenzelm 2005-04-07 Drule.add_used;
2005-04-07 wenzelm 2005-04-07 invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!
2005-04-07 wenzelm 2005-04-07 added add_used; include tpairs;
2005-04-07 wenzelm 2005-04-07 improved exn_message;
2005-04-07 wenzelm 2005-04-07 Thm.invoke_oracle_i;
2005-04-07 wenzelm 2005-04-07 Scan.peek;
2005-04-07 wenzelm 2005-04-07 tuned updates, added map_entry;
2005-04-07 wenzelm 2005-04-07 added some, peek, trace'; tuned;
2005-04-07 wenzelm 2005-04-07 added header;
2005-04-07 wenzelm 2005-04-07 improved comments;
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-04-07 wenzelm 2005-04-07 handle Option instead of OPTION;
2005-04-06 nipkow 2005-04-06 updated it
2005-04-06 quigley 2005-04-06 watcher.ML and watcher.sig changed. Debug files now write to tmp.
2005-04-05 quigley 2005-04-05 Current version of res_atp.ML - causes an error when I run it. C.Q.
2005-04-05 paulson 2005-04-05 lexicographic order by Norbert Voelker
2005-04-05 paulson 2005-04-05 arg_cong2 by Norbert Voelker
2005-04-05 nipkow 2005-04-05 *** empty log message ***
2005-04-04 quigley 2005-04-04 Updated to add watcher code.
2005-04-04 quigley 2005-04-04 CVSfj  ------------------------------------------------------------------- --------------------------------------------------------------- Temporarily added until res_axioms.ML is altered.
2005-04-02 huffman 2005-04-02 Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
2005-04-02 huffman 2005-04-02 converted to new-style theory
2005-04-01 huffman 2005-04-01 convert to new-style theory
2005-04-01 paulson 2005-04-01 x-symbols and other tidying
2005-04-01 skalberg 2005-04-01 Updated import configuration.
2005-04-01 gagern 2005-04-01 bring make to delete files on error
2005-04-01 paulson 2005-04-01 patch to get it working again
2005-03-31 quigley 2005-03-31 *** empty log message ***
2005-03-31 quigley 2005-03-31 *** empty log message ***
2005-03-31 quigley 2005-03-31 *** empty log message ***
2005-03-31 huffman 2005-03-31 added theorems eta_cfun and cont2cont_eta
2005-03-31 huffman 2005-03-31 chfin now a subclass of po, proved instance chfin < cpo
2005-03-31 huffman 2005-03-31 cleaned up some proofs
2005-03-31 huffman 2005-03-31 fixed bug in prj' function
2005-03-31 huffman 2005-03-31 changed comments to text blocks, cleaned up a few proofs
2005-03-30 paulson 2005-03-30 converted from DOS to UNIX format
2005-03-29 paulson 2005-03-29 converted HOL-Subst to tactic scripts
2005-03-28 paulson 2005-03-28 conversion of UNITY to Isar scripts
2005-03-26 paulson 2005-03-26 new display of theory stamps
2005-03-26 gagern 2005-03-26 op vor infix-Konstruktoren im datatype binding zum besseren Parsen
2005-03-26 kleing 2005-03-26 use Library/Multiset instead of own definition
2005-03-26 kleing 2005-03-26 fixed typo (multiset_append) moved multiset_of_complement_union from ex/Sorting
2005-03-25 aspinall 2005-03-25 Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
2005-03-25 paulson 2005-03-25 tidied up
2005-03-25 aspinall 2005-03-25 Revert previous change (but leave comments).
2005-03-25 aspinall 2005-03-25 Support new PGIP commands redostep, redoitem
2005-03-25 aspinall 2005-03-25 Support non-standard file: URL syntax, temporarily.
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-24 ballarin 2005-03-24 *** empty log message ***