2007-10-30 haftmann 2007-10-30 fixed typo
2007-10-30 haftmann 2007-10-30 const antiquotation clarified
2007-10-30 haftmann 2007-10-30 clarified
2007-10-30 haftmann 2007-10-30 handling of notation in class target
2007-10-30 haftmann 2007-10-30 fixed document preparation
2007-10-30 haftmann 2007-10-30 improved website integration
2007-10-30 haftmann 2007-10-30 adjusted
2007-10-30 haftmann 2007-10-30 split library index into templates
2007-10-30 haftmann 2007-10-30 split library index into templates
2007-10-30 haftmann 2007-10-30 structured
2007-10-30 haftmann 2007-10-30 tidied version
2007-10-30 haftmann 2007-10-30 simplified proof
2007-10-30 haftmann 2007-10-30 continued localization
2007-10-29 haftmann 2007-10-29 fixed typo
2007-10-29 haftmann 2007-10-29 added nbe
2007-10-29 wenzelm 2007-10-29 test_proof: do not change Proofterm.proofs here (not thread-safe);
2007-10-29 wenzelm 2007-10-29 improved notion of 'nicer' fact names (observe some name space properties);
2007-10-29 wenzelm 2007-10-29 export is_hidden;
2007-10-29 wenzelm 2007-10-29 added bool_ord;
2007-10-29 wenzelm 2007-10-29 qualified Proofterm.proofs;
2007-10-29 krauss 2007-10-29 fun/function: generate case names for induction rules
2007-10-28 wenzelm 2007-10-28 append/member: more light-weight way to declare authentic syntax; tuned proofs;
2007-10-28 wenzelm 2007-10-28 made SML/NJ happy;
2007-10-28 wenzelm 2007-10-28 safe_exit: controlled_execution;
2007-10-27 obua 2007-10-27 better compute oracle
2007-10-27 obua 2007-10-27 better compute oracle
2007-10-27 obua 2007-10-27 adapted Compute...
2007-10-27 krauss 2007-10-27 use "fun" for definition of "member" -> authentic syntax
2007-10-27 haftmann 2007-10-27 ASCIIfied README
2007-10-27 haftmann 2007-10-27 added list comprehension syntax
2007-10-26 wenzelm 2007-10-26 locale_const: in_class workaround prevents additional locale version of class consts;
2007-10-26 wenzelm 2007-10-26 notation: associate syntax to checked-unchecked term;
2007-10-26 wenzelm 2007-10-26 export class_prefix; removed obsolete const hiding;
2007-10-26 haftmann 2007-10-26 tuned
2007-10-26 haftmann 2007-10-26 changed order of class parameters
2007-10-26 haftmann 2007-10-26 dropped square syntax
2007-10-26 haftmann 2007-10-26 localized monotonicity; tuned syntax
2007-10-26 haftmann 2007-10-26 dropped "brown" syntax
2007-10-26 wenzelm 2007-10-26 replaced Secure.evaluate by ML_Context.evaluate;
2007-10-26 wenzelm 2007-10-26 asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
2007-10-26 wenzelm 2007-10-26 proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
2007-10-26 krauss 2007-10-26 print the defined constants when finished; tuned
2007-10-26 haftmann 2007-10-26 adjusted
2007-10-26 haftmann 2007-10-26 tuned
2007-10-26 krauss 2007-10-26 added NEWS entry for function package
2007-10-26 haftmann 2007-10-26 added hint for algebra
2007-10-25 haftmann 2007-10-25 moved primitive operations to class.ML
2007-10-25 haftmann 2007-10-25 fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
2007-10-25 haftmann 2007-10-25 dropped redundancy
2007-10-25 haftmann 2007-10-25 various localizations
2007-10-25 wenzelm 2007-10-25 made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
2007-10-25 haftmann 2007-10-25 tuned
2007-10-25 haftmann 2007-10-25 clarified implementation
2007-10-25 haftmann 2007-10-25 propagation through class hierarchy
2007-10-25 haftmann 2007-10-25 added function for evaluation by compiler invocation
2007-10-25 haftmann 2007-10-25 more computation with rationals
2007-10-25 haftmann 2007-10-25 localized further
2007-10-25 haftmann 2007-10-25 continued
2007-10-25 haftmann 2007-10-25 tuned
2007-10-24 wenzelm 2007-10-24 THIS_IS_ISABELLE_MAKEBIN;