2000-01-05 wenzelm 2000-01-05 ObtainFun; prepare vars / asms / pats only once;
2000-01-05 wenzelm 2000-01-05 added thms_ctxt_args;
2000-01-05 wenzelm 2000-01-05 prepare patterns only once;
2000-01-05 wenzelm 2000-01-05 ObtainFun;
2000-01-05 wenzelm 2000-01-05 present chapter; tuned proof markup commands; moved obtain to obtain.ML;
2000-01-05 wenzelm 2000-01-05 removed pats;
2000-01-05 wenzelm 2000-01-05 chapter;
2000-01-05 wenzelm 2000-01-05 support for dummy variables (anyT, logicT); improved error msg: meet *before* assign;
2000-01-05 wenzelm 2000-01-05 TypeInfer.logicT;
2000-01-04 oheimb 2000-01-04 new arg type for max_spec etc.
2000-01-03 bauerg 2000-01-03 small changes;
2000-01-03 oheimb 2000-01-03 removed inj_eq from the default simpset again
2000-01-03 oheimb 2000-01-03 removed inj_eq from the default simpset again
1999-12-23 oheimb 1999-12-23 removed inj_eq from the default simpset again
1999-12-23 kleing 1999-12-23 updated sml package name in installation exmaple
1999-12-22 wenzelm 1999-12-22 raw_t(e)xt: any proof mode;
1999-12-22 wenzelm 1999-12-22 fixed error msg;
1999-12-22 wenzelm 1999-12-22 marg_comment: repeat;
1999-12-22 wenzelm 1999-12-22 text: string list;
1999-12-22 paulson 1999-12-22 tidied, with a bit more progress
1999-12-22 paulson 1999-12-22 Working version after a FAILED attempt to base Follows upon LeadsETo
1999-12-22 paulson 1999-12-22 new weakening laws
1999-12-22 paulson 1999-12-22 removing the "{} : CC" requirement for leadsTo[CC]
1999-12-22 kleing 1999-12-22 back to old sml version (due to c library problems)
1999-12-22 kleing 1999-12-22 some tuning (incorporated David's suggestions)
1999-12-21 paulson 1999-12-21 working with weak LeadsTo in guarantees precondition\!
1999-12-21 oheimb 1999-12-21 corrected, improved eMail addresses, user interface section
1999-12-17 paulson 1999-12-17 now workign as far as System_Alloc_Progress
1999-12-16 paulson 1999-12-16 SOUNDNESS BUG FIX for rotate_rule. The original code did not expect nested parameters such as !!y. Goal "!!x. x = a ==> (!!y. y ~= a ==> False)"; by (rotate_tac 1 1); be notE 1; ba 1; qed "foo"; val FalseI = standard (True_not_False RS (standard (refl RS foo)));
1999-12-15 paulson 1999-12-15 first working version to Alloc/System_Client_Progress; uses new "preserves" primitive instead of localTo
1999-12-13 paulson 1999-12-13 expandshort
1999-12-09 kleing 1999-12-09 dist page now in page/dist-{content|layout}
1999-12-09 wenzelm 1999-12-09 updated;
1999-12-09 kleing 1999-12-09 prettyfied
1999-12-09 kleing 1999-12-09 full url to local (munich) page
1999-12-09 kleing 1999-12-09 new web pages integrated
1999-12-09 kleing 1999-12-09 used for new weg page layout
1999-12-09 kleing 1999-12-09 ID line added
1999-12-09 kleing 1999-12-09 new webpage layout
1999-12-08 paulson 1999-12-08 abolition of localTo: instead "guarantees" has local vars as extra argument
1999-12-08 paulson 1999-12-08 used image_eq_UN to speed up slow proofs of base cases
1999-12-08 paulson 1999-12-08 useful lemma eqset_imp_iff
1999-12-07 wenzelm 1999-12-07 tuned;
1999-12-07 wenzelm 1999-12-07 tuned;
1999-12-07 wenzelm 1999-12-07 added Isar_examples/Fibonacci.thy;
1999-12-07 nipkow 1999-12-07 Fixed bug in find-functions: list of parameters must be reversed before subsitution.
1999-12-06 nipkow 1999-12-06 Renamed some vars
1999-12-02 nipkow 1999-12-02 cosmetic mod.
1999-12-01 wenzelm 1999-12-01 accommodate current version of rpm;
1999-12-01 nipkow 1999-12-01 Fixed a problem with returning from the last frame.
1999-12-01 paulson 1999-12-01 new generalized leads-to theory
1999-12-01 paulson 1999-12-01 fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER (for Moscow ML)
1999-11-30 paulson 1999-11-30 deleted rogue copy of localTo_imp_o_localTo
1999-11-30 paulson 1999-11-30 working version with new theory ELT
1999-11-30 paulson 1999-11-30 new theory UNITY/ELT
1999-11-29 wenzelm 1999-11-29 Goal: tuned pris;
1999-11-29 nipkow 1999-11-29 Removed !!
1999-11-29 wenzelm 1999-11-29 Minimal.thy;
1999-11-29 wenzelm 1999-11-29 Isar_examples/Minimal.thy;
1999-11-29 wenzelm 1999-11-29 qed "";