2005-05-31 wenzelm 2005-05-31 tuned;
2005-05-30 wenzelm 2005-05-30 tuned;
2005-05-30 obua 2005-05-30 Infinite chains in definitions are now detected, too.
2005-05-30 kleing 2005-05-30 typo
2005-05-30 kleing 2005-05-30 updated para on searching
2005-05-30 nipkow 2005-05-30 added \nexists
2005-05-29 obua 2005-05-29 Removes an inconsistent definition from Library.thy , so that the lexical order is the standard order for lists. The prefix order is not built any more.
2005-05-29 obua 2005-05-29 Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
2005-05-29 kleing 2005-05-29 make COPYRIGHT file available for web page
2005-05-28 kleing 2005-05-28 path /home/stud doesn't exist on macbroy33 (only /usr/stud)
2005-05-27 ballarin 2005-05-27 SML/NJ compatibility.
2005-05-27 ballarin 2005-05-27 Typo.
2005-05-27 ballarin 2005-05-27 Deleted old code.
2005-05-27 ballarin 2005-05-27 Locale expressions: rename with optional mixfix syntax.
2005-05-27 aspinall 2005-05-27 Add back rudely removed and popular -X option.
2005-05-27 paulson 2005-05-27 Now uses File.write and File.append
2005-05-27 huffman 2005-05-27 removed obsolete theorems
2005-05-27 huffman 2005-05-27 use TypedefPcpo for all class instances
2005-05-27 kleing 2005-05-27 log more failure types
2005-05-27 huffman 2005-05-27 added lemmas monofun_lub_fun and cont_lub_fun
2005-05-27 kleing 2005-05-27 put global isatest settings in one file, sourced by the other scripts
2005-05-27 huffman 2005-05-27 Use TypedefPcpo theorem for po instance
2005-05-27 huffman 2005-05-27 use thelub_const lemma
2005-05-27 huffman 2005-05-27 added lemma thelub_const
2005-05-26 paulson 2005-05-26 further tweaks to the SPASS setup
2005-05-26 paulson 2005-05-26 goodby to modUnix
2005-05-26 paulson 2005-05-26 trying to set up portable calling sequences for SPASS and tptp2X
2005-05-26 kleing 2005-05-26 cleaned up select_match do not return trivial matches made simp: t work
2005-05-26 paulson 2005-05-26 Narrower version of the Proof General's head; removal of the alternative icon and environment
2005-05-26 paulson 2005-05-26 Narrower version of the Proof General's head
2005-05-26 huffman 2005-05-26 rewrote continuous isomorphism section, cleaned up
2005-05-26 huffman 2005-05-26 cleaned up, added UU_app and less_funI, removed some obsolete stuff
2005-05-26 huffman 2005-05-26 added defaultsort declaration, moved cpair_less to Cprod.thy
2005-05-26 huffman 2005-05-26 added defaultsort declaration
2005-05-26 huffman 2005-05-26 cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
2005-05-26 huffman 2005-05-26 removed dependence on Cfun.thy
2005-05-26 huffman 2005-05-26 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
2005-05-25 paulson 2005-05-25 new Brouwer ordinal example
2005-05-25 kleing 2005-05-25 more cleanup
2005-05-25 kleing 2005-05-25 tuned thm_style section
2005-05-25 nipkow 2005-05-25 added ? explanations
2005-05-25 kleing 2005-05-25 renamed search criterion 'rewrite' to 'simp'
2005-05-25 paulson 2005-05-25 SML/NJ compatibility
2005-05-25 paulson 2005-05-25 new environments for Proof General notes
2005-05-25 kleing 2005-05-25 removed obsolete findI, findE, findEs (and the functions they depended on in Isar/find_theorems)
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-05-25 nipkow 2005-05-25 *** empty log message ***
2005-05-25 nipkow 2005-05-25 grammar
2005-05-25 huffman 2005-05-25 shorted proof that lift is chfin
2005-05-25 quigley 2005-05-25 Removed shell variables. Now uses isatool getenv -b SPASS_HOME.
2005-05-24 quigley 2005-05-24 Generic version of spassshell. Add SPASS_HOME to .bashrc so that shell script can find it.
2005-05-24 haftmann 2005-05-24 ML_idf antiquotation
2005-05-24 paulson 2005-05-24 oracle example converted to Isar
2005-05-24 paulson 2005-05-24 cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
2005-05-24 paulson 2005-05-24 A new structure and reduced indentation
2005-05-24 huffman 2005-05-24 Simplified version of strict sum theory, using TypedefPcpo
2005-05-24 huffman 2005-05-24 Simplified version of strict product theory, using TypedefPcpo
2005-05-24 huffman 2005-05-24 New theory for defining subtypes of pcpos
2005-05-24 huffman 2005-05-24 added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
2005-05-24 huffman 2005-05-24 Moved admissibility definitions and lemmas to a separate theory