2007-03-16 haftmann 2007-03-16 updated
2007-03-16 urbanc 2007-03-16 adjusted for the example file SOS.thy
2007-03-16 urbanc 2007-03-16 added formalisations of typical SOS-proofs
2007-03-16 urbanc 2007-03-16 added eqvt-lemmas for integers and eqvt-tagged the lemma append_eqvt
2007-03-16 dixon 2007-03-16 removed safe elim flag of trueElim and notFalseElim for testing.
2007-03-16 dixon 2007-03-16 added safe intro rules for removing "True" subgoals as well as "~ False" ones.
2007-03-14 huffman 2007-03-14 move sqrt_divide_self_eq to NthRoot.thy
2007-03-14 huffman 2007-03-14 move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
2007-03-14 webertj 2007-03-14 is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
2007-03-13 urbanc 2007-03-13 deleted function for defining candidates and used nominal_primrec instead
2007-03-12 wenzelm 2007-03-12 syntax: proper body priorty for derived binders;
2007-03-12 wenzelm 2007-03-12 tuned;
2007-03-12 narboux 2007-03-12 removes some unused code that used to try to derive a simpler version of the eqvt lemmas
2007-03-12 berghofe 2007-03-12 Adapted to new inductive definition package.
2007-03-11 haftmann 2007-03-11 clarified code
2007-03-10 berghofe 2007-03-10 - Replaced fold by fold_rev to make sure that list of predicate variables pvars (for invariants) is in the correct order - Adapted to new format of datatype descriptor
2007-03-10 berghofe 2007-03-10 - Changed format of descriptor contained in nominal_datatype_info - Equivariance proof for graph of primrec combinator no longer uses large simpset (more robust).
2007-03-10 berghofe 2007-03-10 Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.
2007-03-10 berghofe 2007-03-10 Adapted to changes in definition of SUP.
2007-03-10 berghofe 2007-03-10 Generalized version of SUP and INF (with index set).
2007-03-10 berghofe 2007-03-10 Eta-expanded codetype_hook to make SML/NJ happy.
2007-03-09 paulson 2007-03-09 First stab at reconstructing HO problems
2007-03-09 haftmann 2007-03-09 constant names now dependent on executable content
2007-03-09 haftmann 2007-03-09 resolved name clashes
2007-03-09 haftmann 2007-03-09 moved order on functions here
2007-03-09 haftmann 2007-03-09 *** empty log message ***
2007-03-09 haftmann 2007-03-09 dropped code datatype certificates
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-03-06 narboux 2007-03-06 correct typo in latex output
2007-03-06 urbanc 2007-03-06 updated this file to the new infrastructure
2007-03-06 krauss 2007-03-06 fixed function package bug in the handling of multiple guards
2007-03-06 urbanc 2007-03-06 major update of the nominal package; there is now an infrastructure for equivariance lemmas which eases definitions of nominal functions
2007-03-06 kleing 2007-03-06 fix wrong default for find_theorems
2007-03-06 kleing 2007-03-06 document find_theorems syntax change
2007-03-06 kleing 2007-03-06 find_theorems: moved with_dup into the brackets, i.e. find_theorems (20 with_dups) "some term" ..
2007-03-06 kleing 2007-03-06 an O(n log n) version of removing duplicates
2007-03-05 kleing 2007-03-05 clean up var/running dir before spawning new tests
2007-03-05 kleing 2007-03-05 additional settings for isatest runs on various platforms
2007-03-05 kleing 2007-03-05 adjust paths
2007-03-05 kleing 2007-03-05 moved all isatest/cron job related files to own directory
2007-03-05 gagern 2007-03-05 AnnoMaLy related files, as discussed in mails with Gerwin Klein
2007-03-03 aspinall 2007-03-03 Simplify print mode. Support setproverflag.
2007-03-03 aspinall 2007-03-03 Update test for new parse result
2007-03-03 aspinall 2007-03-03 Add setproverflag, to replace other flag controls
2007-03-03 aspinall 2007-03-03 Add objtypes to openblock/closeblock and theory items (can be used to control folding).
2007-03-03 aspinall 2007-03-03 Add more attributes to openblock. Change theory item objtype field to proper objtype.
2007-03-03 aspinall 2007-03-03 Add Isabelle-specific objtypes
2007-03-03 aspinall 2007-03-03 Comment
2007-03-03 haftmann 2007-03-03 clarified code
2007-03-03 haftmann 2007-03-03 clarified error message
2007-03-03 haftmann 2007-03-03 moved instance option :: finite to Finite_Set.thy
2007-03-03 haftmann 2007-03-03 moved instance option :: finite here
2007-03-03 aspinall 2007-03-03 Fix idvalue output and PGML print mode raw encode/decode.
2007-03-02 haftmann 2007-03-02 permitting empty datatypes
2007-03-02 haftmann 2007-03-02 improved handling of nat numerals
2007-03-02 haftmann 2007-03-02 tuned code theorems for ord on integers
2007-03-02 haftmann 2007-03-02 simplified code generator setup
2007-03-02 haftmann 2007-03-02 tuned code theorems
2007-03-02 haftmann 2007-03-02 added add_numerals_of
2007-03-02 haftmann 2007-03-02 now using "class"