1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1998-12-28 paulson 1998-12-28 revised datatype definition package
1998-12-28 paulson 1998-12-28 revised inductive definition package
1998-12-28 paulson 1998-12-28 new primrec package
1998-12-28 paulson 1998-12-28 moved from ZF to new subdirectory Tools
1998-12-28 paulson 1998-12-28 new theorem update_type
1998-12-28 paulson 1998-12-28 converted to use new primrec section and update operator
1998-12-28 paulson 1998-12-28 converted to use new primrec section
1998-12-28 paulson 1998-12-28 fixed comment
1998-12-28 paulson 1998-12-28 Needs separate theory Primrec_defs due to new inductive defs package
1998-12-28 paulson 1998-12-28 more efficient strip_quotes using "substring"
1998-12-28 paulson 1998-12-28 Basis Library compatible substring oeration
1998-12-28 paulson 1998-12-28 Added a "message" argument to print_tac
1998-12-28 paulson 1998-12-28 comments
1998-12-28 paulson 1998-12-28 deleted "escape" and "trim"; Basis Library can do string escapes if necessary
1998-12-28 paulson 1998-12-28 String added to BasisLibrary
1998-12-28 paulson 1998-12-28 better indentation
1998-12-28 paulson 1998-12-28 fixed comments
1998-12-28 paulson 1998-12-28 replaced obsolete "trim" by "strip_quotes"
1998-12-18 nipkow 1998-12-18 Link to HOLCF paper added.
1998-12-18 paulson 1998-12-18 moved dest_Type to term.ML from HOL/Tools/primrec_package
1998-12-18 paulson 1998-12-18 moved dest_eq to hologic.ML and tidied
1998-12-18 paulson 1998-12-18 new function dest_eq
1998-12-17 wenzelm 1998-12-17 tuned mode_name;
1998-12-17 wenzelm 1998-12-17 bash -c :;
1998-12-11 oheimb 1998-12-11 *** empty log message ***
1998-12-11 oheimb 1998-12-11 added new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows)
1998-12-11 oheimb 1998-12-11 better representation of Sigma
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;