1998-09-09 nipkow 1998-09-09 Proved and added rewrite rule (@x. x=y) = y to simpset. Strange that only the symetric version was present!
1998-09-09 oheimb 1998-09-09 reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
1998-09-09 oheimb 1998-09-09 AddIffs[not_None_eq]; made wrapper ospec really safe
1998-09-09 oheimb 1998-09-09 AddSDs[override_SomeD]; replaced map_of_append by map_of_override, changing its direction
1998-09-09 oheimb 1998-09-09 changed constants mem and list_all to mere translations added filter_is_subset
1998-09-09 oheimb 1998-09-09 changed order of included theories
1998-09-09 oheimb 1998-09-09 added Id_apply
1998-09-09 oheimb 1998-09-09 removed superfluous AddIs thms (were already in)
1998-09-09 oheimb 1998-09-09 renamed sswhen to sscase
1998-09-09 oheimb 1998-09-09 simplified definition of axclass cpo
1998-09-08 oheimb 1998-09-08 added caveat; a real solution would be difficult
1998-09-08 oheimb 1998-09-08 improved spacing
1998-09-08 oheimb 1998-09-08 adapted modifiers: Mod1 -> Mod2, Mod5 -> Mod4
1998-09-08 paulson 1998-09-08 Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
1998-09-08 paulson 1998-09-08 Got rid of not_Says_to_self; re-organized proofs
1998-09-07 paulson 1998-09-07 new example; tidying
1998-09-07 paulson 1998-09-07 new example
1998-09-07 paulson 1998-09-07 New UNITY theory, the N-S protocol
1998-09-07 paulson 1998-09-07 tidying
1998-09-04 nipkow 1998-09-04 Function 'upt'
1998-09-04 nipkow 1998-09-04 Arith: less_diff_conv List: [i..j]
1998-09-03 paulson 1998-09-03 A new approach, using simp_of_act and simp_of_set to activate definitions when necessary
1998-09-02 nipkow 1998-09-02 Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.
1998-09-02 paulson 1998-09-02 modified proofs for new constrains_tac and ensures_tac
1998-09-02 paulson 1998-09-02 two new thms
1998-09-02 paulson 1998-09-02 Moved constrains_tac from SubstAx to Constrains. Removed Auto_tac calls from it and ensures_tac
1998-09-02 paulson 1998-09-02 small simplification to not_Says_to_self
1998-09-01 paulson 1998-09-01 New approach, using a locale
1998-09-01 paulson 1998-09-01 tidied
1998-09-01 paulson 1998-09-01 Replaced Suc_diff_n by Suc_diff_le
1998-09-01 paulson 1998-09-01 new theory Induct/FoldSet
1998-09-01 paulson 1998-09-01 New law card_Un_Int. Removed card_insert from simpset
1998-09-01 paulson 1998-09-01 tidying; moved diff_less to Arith.ML
1998-09-01 paulson 1998-09-01 changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
1998-09-01 paulson 1998-09-01 New lemmas involving Int
1998-09-01 paulson 1998-09-01 New lemmas involving Int
1998-09-01 paulson 1998-09-01 fixed error msg
1998-09-01 paulson 1998-09-01 Moved lemmas to Arith.ML
1998-09-01 paulson 1998-09-01 Two new subtraction lemmas
1998-08-30 wenzelm 1998-08-30 made SML/NJ happy;
1998-08-28 wenzelm 1998-08-28 * print mode 'emacs' reserved for Isamode;
1998-08-28 wenzelm 1998-08-28 added emacs mode; tuned;
1998-08-28 wenzelm 1998-08-28 tuned isatool install;
1998-08-28 wenzelm 1998-08-28 tuned;
1998-08-28 wenzelm 1998-08-28 -d DISTDIR; tuned;
1998-08-28 wenzelm 1998-08-28 tuned;
1998-08-27 wenzelm 1998-08-27 www.in.tum.de;
1998-08-27 wenzelm 1998-08-27 made tutorial first;
1998-08-27 wenzelm 1998-08-27 tuned;
1998-08-27 wenzelm 1998-08-27 exec;
1998-08-27 wenzelm 1998-08-27 * Pure: ML function 'theory_of' replaced by 'theory';
1998-08-27 wenzelm 1998-08-27 tuned;
1998-08-27 wenzelm 1998-08-27 isatool install;
1998-08-27 wenzelm 1998-08-27 added tutorial;
1998-08-27 wenzelm 1998-08-27 fixed ISABELLE_USEDIR_OPTIONS;
1998-08-27 wenzelm 1998-08-27 *** empty log message ***
1998-08-27 wenzelm 1998-08-27 Goal, Goalw; thm, thms; moved get_thm etc. from theories.tex;
1998-08-27 wenzelm 1998-08-27 moeved get_thm etc. to goals.tex;
1998-08-27 wenzelm 1998-08-27 tuned doc name;
1998-08-27 wenzelm 1998-08-27 fixed center;