2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2003-08-29 skalberg 2003-08-29 Removed the extended digits again.
2003-08-28 skalberg 2003-08-28 Fixed typos.
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2003-08-27 skalberg 2003-08-27 Added skalberg to recepients, changed admin from kleing to berghofe.
2003-08-27 skalberg 2003-08-27 Converted to new style theories.
2003-08-27 skalberg 2003-08-27 Prepared for extended identifiers (\<alpha>, etc.)
2003-08-27 skalberg 2003-08-27 Improved the error messages (slightly).
2003-08-26 skalberg 2003-08-26 Cleaned up the code.
2003-08-26 skalberg 2003-08-26 New specification syntax added (the specification may be split over several properties).
2003-08-26 skalberg 2003-08-26 Allowed for splitting the specification over several lemmas.
2003-08-22 berghofe 2003-08-22 Improved handling of modes for equality predicate, to avoid ill-typed ML code due to comparisons between elements of function types.
2003-08-21 berghofe 2003-08-21 Fixed problem with "code ind" attribute that caused code generator to fail for mutually recursive predicates.
2003-08-21 berghofe 2003-08-21 Added function strong_conn for computing the strongly connected components of the graph.
2003-08-21 paulson 2003-08-21 Change from "tracing" to "warning", as requested by David Aspinall
2003-08-20 paulson 2003-08-20 final tweaks for Isar version
2003-08-20 paulson 2003-08-20 finished conversion to Isar format
2003-08-20 paulson 2003-08-20 new example
2003-08-20 paulson 2003-08-20 new case_tac method
2003-08-20 paulson 2003-08-20 partial conversion to Isar format
2003-08-19 paulson 2003-08-19 partial conversion to Isar format
2003-08-19 paulson 2003-08-19 new case_tac
2003-08-19 paulson 2003-08-19 For the Isar version of the ZF logics manual
2003-08-15 paulson 2003-08-15 converting ex/If to Isar script
2003-08-15 paulson 2003-08-15 A document for UNITY
2003-08-13 paulson 2003-08-13 reformatting change and mention of Introduction to Isabelle
2003-08-13 paulson 2003-08-13 corrections by Viktor Kuncak and minor updating
2003-08-13 paulson 2003-08-13 added tutorial
2003-08-13 paulson 2003-08-13 possibility proof!
2003-08-12 paulson 2003-08-12 ZhouGollmann: new example (fair non-repudiation protocol)
2003-08-08 streckem 2003-08-08 added lemma c_hupd_fst
2003-08-08 streckem 2003-08-08 Modifications after changes in MicroJava/J
2003-08-08 streckem 2003-08-08 Changed lemmas .._type_sound
2003-08-08 streckem 2003-08-08 Added lemma exec_no_xcpt
2003-08-07 berghofe 2003-08-07 test_term now renames variable for size of test data to avoid clashes with variables already present in the term to be tested.
2003-08-05 nipkow 2003-08-05 cleaned up
2003-07-31 nipkow 2003-07-31 *** empty log message ***
2003-07-31 berghofe 2003-07-31 Removed extraneous rev in function goal_params (the list of parameters is already reversed by rename_wrt_term).
2003-07-29 kleing 2003-07-29 opened new section for next Isabelle release
2003-07-28 berghofe 2003-07-28 test_term now handles Match exception raised in generated code.
2003-07-25 nipkow 2003-07-25 Replaced \<leadsto> by \<rightharpoonup>
2003-07-25 paulson 2003-07-25 Simplified a proof using presburger
2003-07-24 paulson 2003-07-24 new theory Library/NatPair
2003-07-24 paulson 2003-07-24 declarations moved from PreList.thy
2003-07-24 berghofe 2003-07-24 Fixed two bugs: - presburger_tac now calls ObjectLogic.atomize_tac first to avoid failure when premises contain meta-level quantifiers or implications - The preprocessor now also filters out premises containing variables that are not of type int or nat.
2003-07-24 berghofe 2003-07-24 Exported function get_mode.
2003-07-24 paulson 2003-07-24 header comment
2003-07-24 paulson 2003-07-24 new theory NatPair of the injection from nat*nat -> nat
2003-07-24 paulson 2003-07-24 Tidying and replacement of some axioms by specifications
2003-07-24 paulson 2003-07-24 tidied
2003-07-22 paulson 2003-07-22 Added some regression testing for simprocs
2003-07-22 paulson 2003-07-22 fixed simprocs
2003-07-21 skalberg 2003-07-21 Added handling of meta implication and meta quantification.
2003-07-21 skalberg 2003-07-21 Added handling of free variables (provided they are of sort HOL.type).
2003-07-21 paulson 2003-07-21 Tidied some examples
2003-07-21 skalberg 2003-07-21 Added the specification command.
2003-07-21 skalberg 2003-07-21 Changed bstring argument to xstring.
2003-07-21 skalberg 2003-07-21 *** empty log message ***
2003-07-19 skalberg 2003-07-19 Added optional theorem names for the constant definitions added during specification.
2003-07-17 skalberg 2003-07-17 Added package for definition by specification.