2004-12-10 aspinall 2004-12-10 Insert pgmltext element into responses in PGIP mode
2004-12-10 berghofe 2004-12-10 Added term cache to function condrew in order to speed up rewriting.
2004-12-10 berghofe 2004-12-10 - Exported functions new_name and new_names - Fixed incompatible signatures problem in unfold_attr
2004-12-10 berghofe 2004-12-10 Fixed bug in mk_gen_of_def that could cause non-termination of the generator for datatypes with nested recursion (such as trie).
2004-12-10 berghofe 2004-12-10 Preprocessors now transfer theorems to current theory in order to avoid "incompatible signatures" exception.
2004-12-10 berghofe 2004-12-10 Moved code generator setup for product type to Product_Type.thy
2004-12-10 berghofe 2004-12-10 New code generator for let and split.
2004-12-10 berghofe 2004-12-10 Realizer for exE now uses let instead of case.
2004-12-09 nipkow 2004-12-09 First step in reorganizing Finite_Set
2004-12-09 paulson 2004-12-09 converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
2004-12-09 paulson 2004-12-09 Comments and other tweaks by Jia
2004-12-09 nipkow 2004-12-09 *** empty log message ***
2004-12-09 paulson 2004-12-09 converted Datatype_Universe to new-style theory
2004-12-08 nipkow 2004-12-08 fixed bug in find functions that I introduced some time ago.
2004-12-08 paulson 2004-12-08 converted Lfp to new-style theory
2004-12-08 kleing 2004-12-08 improvements by Larry and Micheal Wahler
2004-12-07 paulson 2004-12-07 renamed attributes to lower case
2004-12-07 paulson 2004-12-07 made proofs more robust
2004-12-07 paulson 2004-12-07 all theories must be related to Reconstruction
2004-12-07 paulson 2004-12-07 converted Gfp to new-style theory
2004-12-07 paulson 2004-12-07 proof of subst by S Merz
2004-12-07 webertj 2004-12-07 comment added
2004-12-07 kleing 2004-12-07 link to tar.gz
2004-12-07 paulson 2004-12-07 proof of subst by S Merz
2004-12-06 nipkow 2004-12-06 Started to clean up and generalize FiniteSet
2004-12-06 kleing 2004-12-06 add latex sugar
2004-12-06 kleing 2004-12-06 moved to Sugar
2004-12-06 kleing 2004-12-06 fixed typos
2004-12-06 kleing 2004-12-06 ignore generated
2004-12-03 paulson 2004-12-03 fixes to clause conversion
2004-12-03 paulson 2004-12-03 trying to fix the transfer problem
2004-12-03 paulson 2004-12-03 tidied
2004-12-03 kleing 2004-12-03 tuned
2004-12-03 kleing 2004-12-03 fixed typo
2004-12-03 kleing 2004-12-03 more sugar
2004-12-02 paulson 2004-12-02 clauses counted from 0
2004-12-02 nipkow 2004-12-02 *** empty log message ***
2004-12-02 nipkow 2004-12-02 Fixed print translation for ALL x > y etc
2004-12-02 nipkow 2004-12-02 added ALL print-translation for > and >=.
2004-12-02 nipkow 2004-12-02 *** empty log message ***
2004-12-02 nipkow 2004-12-02 Added "ALL x > y" and relatives.
2004-12-02 paulson 2004-12-02 new CLAUSIFY attribute for proof reconstruction with lemmas
2004-12-02 nipkow 2004-12-02 *** empty log message ***
2004-12-02 kleing 2004-12-02 antiquotations lhs and rhs
2004-12-01 nipkow 2004-12-01 *** empty log message ***
2004-12-01 nipkow 2004-12-01 Removed postfix >= because of new >= sugar
2004-12-01 nipkow 2004-12-01 Added > and >= sugar
2004-12-01 nipkow 2004-12-01 >= became > = because of new >=
2004-12-01 paulson 2004-12-01 fixed presentation
2004-12-01 paulson 2004-12-01 resolution package tools by Jia Meng
2004-12-01 kleing 2004-12-01 new antiquotations @{lhs thm} and @{rhs thm}
2004-12-01 kleing 2004-12-01 added antiquotations @{lhs thm} and @{rhs thm}
2004-12-01 kleing 2004-12-01 fixed another _
2004-11-30 paulson 2004-11-30 resolution package tools by Jia Meng
2004-11-30 paulson 2004-11-30 converted Wellfounded_Relations to Isar script
2004-11-30 schirmer 2004-11-30 even more mboxes
2004-11-30 schirmer 2004-11-30 Rule: put \mbox around premises/conclusion to avoid problems with super/sub-scripts.
2004-11-30 kleing 2004-11-30 blast_tac -> blast in comment (fix latex error)
2004-11-29 nipkow 2004-11-29 *** empty log message ***
2004-11-29 paulson 2004-11-29 converted to Isar script, simplifying some results