2006-10-06 paulson 2006-10-06 Tidied code to delete tmp files. Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
2006-10-06 paulson 2006-10-06 renamed the combinator laws
2006-10-06 paulson 2006-10-06 Improved detection of identical clauses, also in the conjecture
2006-10-06 paulson 2006-10-06 Refinements to abstraction. Seeding with combinators K, I and B.
2006-10-06 kleing 2006-10-06 examples for hex and bin numerals
2006-10-05 mengj 2006-10-05 Changed and removed some functions related to combinators, since they are Isabelle constants now.
2006-10-05 paulson 2006-10-05 Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
2006-10-05 paulson 2006-10-05 improvements to abstraction, ensuring more re-use of abstraction functions moving some functions to Pure/drule.ML
2006-10-05 paulson 2006-10-05 facts about combinators
2006-10-05 paulson 2006-10-05 a few new functions on thms and cterms
2006-10-05 huffman 2006-10-05 reorganize and speed up termdiffs proofs
2006-10-04 nipkow 2006-10-04 fixed bug in linear arith
2006-10-04 haftmann 2006-10-04 improvements for Haskell serialization
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-10-04 haftmann 2006-10-04 cleaned up some mess
2006-10-04 haftmann 2006-10-04 clarified header comments
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-10-04 haftmann 2006-10-04 *** empty log message ***
2006-10-04 webertj 2006-10-04 tuned
2006-10-04 krauss 2006-10-04 Improved error reporting
2006-10-04 webertj 2006-10-04 nnf_simpset built statically
2006-10-03 huffman 2006-10-03 rewrite proofs of powser_insidea and termdiffs_aux
2006-10-02 huffman 2006-10-02 generalize summability lemmas using class banach
2006-10-02 haftmann 2006-10-02 clarified setup name
2006-10-02 haftmann 2006-10-02 various code refinements
2006-10-02 haftmann 2006-10-02 fixed some Haskell issues
2006-10-02 haftmann 2006-10-02 changed preprocessing framework
2006-10-02 haftmann 2006-10-02 clarified some things
2006-10-02 haftmann 2006-10-02 cleaned and extended
2006-10-02 haftmann 2006-10-02 added gen_primrec
2006-10-02 haftmann 2006-10-02 added code for insert
2006-10-02 haftmann 2006-10-02 improvements for code_gen
2006-10-02 haftmann 2006-10-02 cleaned mess
2006-10-02 haftmann 2006-10-02 added example for code_gen
2006-10-02 haftmann 2006-10-02 dropped obsolete Theory.sign_of
2006-10-02 haftmann 2006-10-02 tuned
2006-10-02 haftmann 2006-10-02 added code generator names for nat_rec and nat_case
2006-10-02 haftmann 2006-10-02 improved serialization for arbitrary
2006-10-02 haftmann 2006-10-02 normal_form now a diagnostic command
2006-10-02 haftmann 2006-10-02 restructured contents
2006-10-02 huffman 2006-10-02 add axclass banach for complete normed vector spaces
2006-10-02 huffman 2006-10-02 remove unused Cauchy_Bseq lemmas
2006-10-02 huffman 2006-10-02 add lemmas norm_not_less_zero, norm_le_zero_iff
2006-10-02 paulson 2006-10-02 added is_Trueprop
2006-10-02 paulson 2006-10-02 tidying and simplifying
2006-10-02 paulson 2006-10-02 Changing the default for theory_const
2006-10-02 paulson 2006-10-02 extensions for Susanto
2006-10-02 paulson 2006-10-02 restored the "length of name > 2" check for package definitions
2006-10-02 paulson 2006-10-02 Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
2006-10-01 wenzelm 2006-10-01 exists_name: include this theory name;
2006-10-01 wenzelm 2006-10-01 removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-10-01 wenzelm 2006-10-01 merged with theory Datatype_Universe;
2006-10-01 wenzelm 2006-10-01 obsolete;
2006-10-01 wenzelm 2006-10-01 renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
2006-10-01 wenzelm 2006-10-01 removed share_data; tuned;
2006-10-01 wenzelm 2006-10-01 cterm_match: avoid recalculation of maxidx;
2006-10-01 wenzelm 2006-10-01 reverted to revision 1.28;
2006-10-01 wenzelm 2006-10-01 proper use of svc_oracle.ML;
2006-10-01 wenzelm 2006-10-01 reactivated theory PER; removed obsolete StringEx;
2006-10-01 wenzelm 2006-10-01 tuned proofs;