1998-12-11 oheimb 1998-12-11 initisaterm now obsolete changed modifiers
1998-12-11 paulson 1998-12-11 new Close_locale synatx
1998-12-11 paulson 1998-12-11 deleted unclosed comment
1998-12-11 paulson 1998-12-11 the + facility for locales, by Florian
1998-12-11 paulson 1998-12-11 new Close_locale synatx
1998-12-07 paulson 1998-12-07 towards handling sharing of variables
1998-12-07 paulson 1998-12-07 tidying
1998-12-07 paulson 1998-12-07 expandshort
1998-12-04 paulson 1998-12-04 better export for nested locales
1998-12-04 paulson 1998-12-04 new (and generalized) theorems about Sigma/Times
1998-12-04 paulson 1998-12-04 locales: assumes and defines may be empty
1998-12-04 paulson 1998-12-04 locales
1998-12-03 wenzelm 1998-12-03 and_list;
1998-12-03 paulson 1998-12-03 Addition of the States component; parts of Comp not working
1998-12-02 wenzelm 1998-12-02 tuned;
1998-12-02 wenzelm 1998-12-02 IOA-Storage: Memory storage case study.
1998-12-02 wenzelm 1998-12-02 Memory storage case study.
1998-12-02 mueller 1998-12-02 Memory storage case study from PhD p.240;
1998-12-02 paulson 1998-12-02 new theorem Pow_UNIV
1998-12-02 paulson 1998-12-02 new rule rev_bexI
1998-12-02 paulson 1998-12-02 new theorems Domain_Union, Range_Union
1998-12-01 wenzelm 1998-12-01 removed duplicate contrapos;
1998-12-01 wenzelm 1998-12-01 enum: !!! after seperator;
1998-12-01 wenzelm 1998-12-01 excursion: ERROR_MESSAGE; exn_message: ERROR;
1998-12-01 wenzelm 1998-12-01 qed: kind_name (again);
1998-12-01 wenzelm 1998-12-01 show_tags flag;
1998-12-01 paulson 1998-12-01 new theorem INT_Un
1998-12-01 paulson 1998-12-01 better version of Image_diag
1998-11-30 paulson 1998-11-30 tactical CHANGED now uses alpha-eta conversion, not alpha conversion Streamlined code
1998-11-30 paulson 1998-11-30 Renamed subset_Sigma_llist to subset_Times_llist
1998-11-30 paulson 1998-11-30 new theorems about diag
1998-11-29 wenzelm 1998-11-29 fixed declatation of patterns and skolem;
1998-11-29 wenzelm 1998-11-29 tuned print_state; changed solve semantics: support back-pressure of asms (cut, def etc.);
1998-11-29 wenzelm 1998-11-29 tuned welcome msg;
1998-11-29 wenzelm 1998-11-29 added restart;
1998-11-29 wenzelm 1998-11-29 added exception RESTART;
1998-11-29 wenzelm 1998-11-29 proof_general_trans (experimental);
1998-11-29 wenzelm 1998-11-29 replaced wakeup by decorate_prompt_fn;
1998-11-29 wenzelm 1998-11-29 eliminated "Trying to recover ..." msg;
1998-11-29 wenzelm 1998-11-29 added oct_char;
1998-11-29 wenzelm 1998-11-29 method brute_force = ALLGOALS force_tac;
1998-11-27 nipkow 1998-11-27 *** empty log message ***
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-11-27 nipkow 1998-11-27 Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
1998-11-27 paulson 1998-11-27 fixed a link
1998-11-27 paulson 1998-11-27 added Real/Hyperreal
1998-11-27 paulson 1998-11-27 Addition of Hyperreal theories Zorn and Filter
1998-11-27 paulson 1998-11-27 moved diag (diagonal relation) from Univ to Relation
1998-11-26 paulson 1998-11-26 tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules
1998-11-26 mueller 1998-11-26 tuning to assimiliate it with PhD;
1998-11-26 nipkow 1998-11-26 Added a general refutation tactic which works by putting things into nnf first.
1998-11-26 nipkow 1998-11-26 Added filter_prems_tac
1998-11-25 wenzelm 1998-11-25 removed prs / prs_fn;
1998-11-25 paulson 1998-11-25 guarantees laws
1998-11-25 paulson 1998-11-25 simplified ensures_UNIV
1998-11-25 paulson 1998-11-25 new thms for invariant
1998-11-25 paulson 1998-11-25 new theorem program_equalityE
1998-11-25 paulson 1998-11-25 renamed vars
1998-11-25 paulson 1998-11-25 image_id in simpset
1998-11-25 wenzelm 1998-11-25 removed prs / prs_fn (broken, because it did not include \n in its semantics, forcing writeln to add one uncoditionally); replaced prs_fn by writeln fn;