2005-06-29 wenzelm 2005-06-29 Syntax.read thy;
2005-06-29 wenzelm 2005-06-29 tuned sort_ord: pointer_eq; tuned size_of_term: less stack usage;
2005-06-29 wenzelm 2005-06-29 removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort; added efficient operations on ordered lists: eq_set, union, subtract, insert_sort/typ(s)/term(s);
2005-06-29 wenzelm 2005-06-29 eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
2005-06-29 wenzelm 2005-06-29 replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
2005-06-29 wenzelm 2005-06-29 added implies_intr_hyps (from thm.ML);
2005-06-29 wenzelm 2005-06-29 added joinable;
2005-06-28 paulson 2005-06-28 stylistic improvements
2005-06-28 haftmann 2005-06-28 added project information in overview
2005-06-28 haftmann 2005-06-28 added project information in overview
2005-06-28 haftmann 2005-06-28 more sophisticated pypager
2005-06-28 paulson 2005-06-28 first-order check now allows quantifiers
2005-06-28 paulson 2005-06-28 stricter first-order check for meson
2005-06-28 paulson 2005-06-28 Constant "If" is now local
2005-06-28 haftmann 2005-06-28 more sophisticated pypager
2005-06-28 paulson 2005-06-28 replacing zabs_def by abs_if
2005-06-28 haftmann 2005-06-28 introduced a notion of mirrors
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 some minor improvements
2005-06-28 haftmann 2005-06-28 corrected comment
2005-06-28 haftmann 2005-06-28 some corrections
2005-06-26 wenzelm 2005-06-26 export get_calculation;
2005-06-25 nipkow 2005-06-25 Added term_lpo
2005-06-25 nipkow 2005-06-25 cancels completely within terms as well now.
2005-06-25 nipkow 2005-06-25 Changes due to new abel_cancel.ML
2005-06-25 kleing 2005-06-25 use both processors on macbroy5
2005-06-25 kleing 2005-06-25 switch mac test to macbroy5
2005-06-25 huffman 2005-06-25 cleaned up
2005-06-25 huffman 2005-06-25 cleaned up proof of contlub_abstraction
2005-06-24 paulson 2005-06-24 meson method taking an argument list
2005-06-24 paulson 2005-06-24 deleted a redundant "use" line
2005-06-24 paulson 2005-06-24 tidying
2005-06-24 paulson 2005-06-24 stylistic tweaks concerning Find
2005-06-24 kleing 2005-06-24 shortened time out by 3h (gives up at 12:00h now). test should be finished by 10:00h usually.
2005-06-24 kleing 2005-06-24 made su[bp]/isu[bp] behave the same as their bsu[bp]..esu[bp] counterparts, properly respect isastylescript now
2005-06-24 kleing 2005-06-24 needed for Isabelle independent build
2005-06-23 huffman 2005-06-23 added theorems fix_strict, fix_defined, fix_id, fix_const
2005-06-23 huffman 2005-06-23 add binder syntax for flift1
2005-06-23 huffman 2005-06-23 add new file to test fixrec package
2005-06-23 huffman 2005-06-23 add csplit3, ssplit3, fup3 as simp rules
2005-06-23 huffman 2005-06-23 New features: permissive option for fixrec to skip proofs of equations; side conditions for fixrec equations (for definedness); fixpat theorem names apply to entire group of theorems; improved error messages
2005-06-23 huffman 2005-06-23 added match functions for spair, sinl, sinr
2005-06-23 nipkow 2005-06-23 fixed \<Prod> syntax
2005-06-23 nipkow 2005-06-23 new
2005-06-22 quigley 2005-06-22 Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers. Will now signal if ATP has run out of time and then kill the watcher.
2005-06-22 wenzelm 2005-06-22 * Pure: the Isar proof context type is already defined early in Pure as Context.proof;
2005-06-22 nipkow 2005-06-22 added find2
2005-06-22 nipkow 2005-06-22 *** empty log message ***
2005-06-22 nipkow 2005-06-22 tunes Find
2005-06-22 nipkow 2005-06-22 added Rules/find2
2005-06-22 wenzelm 2005-06-22 tuned pointer_eq;
2005-06-22 wenzelm 2005-06-22 renamed data kind;