1998-09-24 oheimb 1998-09-24 simplified CLASIMP_DATA renamed mk_meta_eq to mk_eq, meta_eq to mk_meta_eq
1998-09-24 paulson 1998-09-24 renamed some axioms; some new theorems
1998-09-24 oheimb 1998-09-24 introduced addSE2, addSD2, addE2, and addD2 reflected changes to addbefore, addSbefore described setup of clasimp.ML introduced clarsimp_tac and Clarsimp_tac
1998-09-24 oheimb 1998-09-24 improved description of looper and splitter reflected changes of mk_meta_eq, ...
1998-09-24 oheimb 1998-09-24 workaround for litte bug in our ln command
1998-09-24 paulson 1998-09-24 Function nat_of now maps negative integers to zero, not their absolute value
1998-09-24 paulson 1998-09-24 renamed some axioms
1998-09-24 paulson 1998-09-24 added correctness proofs for arithmetic
1998-09-24 paulson 1998-09-24 new induction rule for integers
1998-09-24 oheimb 1998-09-24 fixed calls of ln, rm
1998-09-23 wenzelm 1998-09-23 changed xnum token syntax;
1998-09-23 paulson 1998-09-23 unary minus
1998-09-23 paulson 1998-09-23 much renaming and reorganization
1998-09-23 paulson 1998-09-23 New directory Integ for the integers
1998-09-23 paulson 1998-09-23 a few new theorems
1998-09-23 paulson 1998-09-23 deleted needless parentheses
1998-09-23 paulson 1998-09-23 tidying and deleting needless parentheses
1998-09-23 paulson 1998-09-23 deleted needless parentheses
1998-09-22 wenzelm 1998-09-22 tuned Isamode;
1998-09-22 paulson 1998-09-22 re-organized for the new directory Integ
1998-09-22 paulson 1998-09-22 new directory for Integers
1998-09-22 paulson 1998-09-22 deleted erroneous semicolon
1998-09-22 paulson 1998-09-22 tidying
1998-09-22 paulson 1998-09-22 tidying
1998-09-22 paulson 1998-09-22 new directory for Integers
1998-09-22 paulson 1998-09-22 big tidying of simpsets, etc
1998-09-21 oheimb 1998-09-21 *** empty log message ***
1998-09-21 oheimb 1998-09-21 improved addbefore and addSbefore improved mechanism for unsafe wrappers
1998-09-21 oheimb 1998-09-21 *** empty log message ***
1998-09-21 oheimb 1998-09-21 added addD2, addE2, addSD2, and addSE2 improved addbefore and addSbefore improved mechanism for unsafe wrappers
1998-09-21 oheimb 1998-09-21 improved indentation
1998-09-21 oheimb 1998-09-21 added wrapper for bspec
1998-09-21 oheimb 1998-09-21 added addD2, addE2, addSD2, and addSE2 added not_Some_eq, also to simpset() and claset()
1998-09-21 oheimb 1998-09-21 re-added mem and list_all improved indentation improved addbefore and addSbefore improved mechanism for unsafe wrappers
1998-09-21 oheimb 1998-09-21 re-added mem and list_all
1998-09-21 oheimb 1998-09-21 added dependance on HOL
1998-09-21 oheimb 1998-09-21 added indentation
1998-09-21 oheimb 1998-09-21 simplified proof
1998-09-21 paulson 1998-09-21 inserted space in #-1 to prevent confusion with an integer constant
1998-09-21 paulson 1998-09-21 Unary minus is now #- and not #~
1998-09-21 paulson 1998-09-21 much renaming and tidying
1998-09-18 paulson 1998-09-18 leaves subgoal package empty
1998-09-18 paulson 1998-09-18 improved (but still flawed) treatment of binary arithmetic
1998-09-18 paulson 1998-09-18 Now defines "int" as a linear order; basic derivations moved to IntDef
1998-09-18 paulson 1998-09-18 new files in Integ
1998-09-18 paulson 1998-09-18 simpler definition of zmagnitude, and new thms for it
1998-09-18 paulson 1998-09-18 stronger version of theI2
1998-09-18 paulson 1998-09-18 tidied
1998-09-18 paulson 1998-09-18 new theorem less_imp_Suc_add
1998-09-18 paulson 1998-09-18 new files in Integ
1998-09-18 paulson 1998-09-18 new theorem less_Suc_eq_le
1998-09-18 paulson 1998-09-18 new files in Integ
1998-09-18 paulson 1998-09-18 new theorem less_Suc_eq_le and le_simps
1998-09-18 paulson 1998-09-18 updated comments
1998-09-18 paulson 1998-09-18 tidying
1998-09-18 paulson 1998-09-18 theorem le_diff_conv2; tidying and expandshort
1998-09-18 paulson 1998-09-18 Pruning of parameters and True assumptions
1998-09-18 paulson 1998-09-18 Suppress timing messages for theorems proved in theory sections
1998-09-18 paulson 1998-09-18 improved error messages
1998-09-16 paulson 1998-09-16 deleted redundant quantifiers