paulson [Fri, 25 Sep 1998 14:06:00 +0200] rev 5567
deleted illegal "op"
paulson [Fri, 25 Sep 1998 14:05:34 +0200] rev 5566
uses BasisLibrary for Int.min
paulson [Fri, 25 Sep 1998 14:05:13 +0200] rev 5565
patched obsolete code
paulson [Fri, 25 Sep 1998 14:04:22 +0200] rev 5564
Renaming of Integ/Integ.* to Integ/Int.*
paulson [Fri, 25 Sep 1998 13:58:24 +0200] rev 5563
Now uses integers instead of naturals
paulson [Fri, 25 Sep 1998 13:57:01 +0200] rev 5562
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson [Fri, 25 Sep 1998 13:18:07 +0200] rev 5561
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
wenzelm [Fri, 25 Sep 1998 12:12:07 +0200] rev 5560
tuned;
wenzelm [Fri, 25 Sep 1998 12:03:11 +0200] rev 5559
tuned pretty_tag;
tag attribute: append;
wenzelm [Fri, 25 Sep 1998 12:01:47 +0200] rev 5558
added REPEAT1;
wenzelm [Thu, 24 Sep 1998 21:32:12 +0200] rev 5557
create an instance of the Isabelle logo;
wenzelm [Thu, 24 Sep 1998 21:19:01 +0200] rev 5556
generic eps version;
oheimb [Thu, 24 Sep 1998 17:18:33 +0200] rev 5555
simplified CLASIMP_DATA
renamed mk_meta_eq to mk_eq
introduced new mk_meta_eq,
simplified addcongs and delcongs, introducing mk_meta_cong
oheimb [Thu, 24 Sep 1998 17:17:56 +0200] rev 5554
removed addcongs2 and delcongs2
simplified CLASIMP_DATA
oheimb [Thu, 24 Sep 1998 17:17:14 +0200] rev 5553
renamed mk_meta_eq to mk_eq
oheimb [Thu, 24 Sep 1998 17:16:06 +0200] rev 5552
simplified CLASIMP_DATA
renamed mk_meta_eq to mk_eq, meta_eq to mk_meta_eq
paulson [Thu, 24 Sep 1998 17:07:24 +0200] rev 5551
renamed some axioms; some new theorems
oheimb [Thu, 24 Sep 1998 16:53:14 +0200] rev 5550
introduced addSE2, addSD2, addE2, and addD2
reflected changes to addbefore, addSbefore
described setup of clasimp.ML
introduced clarsimp_tac and Clarsimp_tac
oheimb [Thu, 24 Sep 1998 16:53:00 +0200] rev 5549
improved description of looper and splitter
reflected changes of mk_meta_eq, ...
oheimb [Thu, 24 Sep 1998 15:36:16 +0200] rev 5548
workaround for litte bug in our ln command
paulson [Thu, 24 Sep 1998 15:23:47 +0200] rev 5547
Function nat_of now maps negative integers to zero, not their absolute value
paulson [Thu, 24 Sep 1998 15:21:30 +0200] rev 5546
renamed some axioms
paulson [Thu, 24 Sep 1998 15:20:29 +0200] rev 5545
added correctness proofs for arithmetic
paulson [Thu, 24 Sep 1998 15:20:03 +0200] rev 5544
new induction rule for integers
oheimb [Thu, 24 Sep 1998 11:00:07 +0200] rev 5543
fixed calls of ln, rm
wenzelm [Wed, 23 Sep 1998 12:44:30 +0200] rev 5542
changed xnum token syntax;
paulson [Wed, 23 Sep 1998 10:56:08 +0200] rev 5541
unary minus
paulson [Wed, 23 Sep 1998 10:25:37 +0200] rev 5540
much renaming and reorganization
paulson [Wed, 23 Sep 1998 10:17:11 +0200] rev 5539
New directory Integ for the integers
paulson [Wed, 23 Sep 1998 10:15:09 +0200] rev 5538
a few new theorems
paulson [Wed, 23 Sep 1998 10:12:01 +0200] rev 5537
deleted needless parentheses
paulson [Wed, 23 Sep 1998 10:11:18 +0200] rev 5536
tidying and deleting needless parentheses
paulson [Wed, 23 Sep 1998 10:03:32 +0200] rev 5535
deleted needless parentheses
wenzelm [Tue, 22 Sep 1998 17:08:30 +0200] rev 5534
tuned Isamode;
paulson [Tue, 22 Sep 1998 15:24:39 +0200] rev 5533
re-organized for the new directory Integ
paulson [Tue, 22 Sep 1998 15:24:01 +0200] rev 5532
new directory for Integers
paulson [Tue, 22 Sep 1998 15:23:39 +0200] rev 5531
deleted erroneous semicolon
paulson [Tue, 22 Sep 1998 15:22:18 +0200] rev 5530
tidying
paulson [Tue, 22 Sep 1998 13:50:57 +0200] rev 5529
tidying
paulson [Tue, 22 Sep 1998 13:49:22 +0200] rev 5528
new directory for Integers
paulson [Tue, 22 Sep 1998 13:48:32 +0200] rev 5527
big tidying of simpsets, etc
oheimb [Mon, 21 Sep 1998 23:25:27 +0200] rev 5526
*** empty log message ***
oheimb [Mon, 21 Sep 1998 23:17:28 +0200] rev 5525
improved addbefore and addSbefore
improved mechanism for unsafe wrappers
oheimb [Mon, 21 Sep 1998 23:16:25 +0200] rev 5524
*** empty log message ***
oheimb [Mon, 21 Sep 1998 23:14:33 +0200] rev 5523
added addD2, addE2, addSD2, and addSE2
improved addbefore and addSbefore
improved mechanism for unsafe wrappers
oheimb [Mon, 21 Sep 1998 23:13:28 +0200] rev 5522
improved indentation
oheimb [Mon, 21 Sep 1998 23:12:31 +0200] rev 5521
added wrapper for bspec
oheimb [Mon, 21 Sep 1998 23:06:37 +0200] rev 5520
added addD2, addE2, addSD2, and addSE2
added not_Some_eq, also to simpset() and claset()
oheimb [Mon, 21 Sep 1998 23:04:51 +0200] rev 5519
re-added mem and list_all
improved indentation
improved addbefore and addSbefore
improved mechanism for unsafe wrappers
oheimb [Mon, 21 Sep 1998 23:03:11 +0200] rev 5518
re-added mem and list_all
oheimb [Mon, 21 Sep 1998 22:58:43 +0200] rev 5517
added dependance on HOL
oheimb [Mon, 21 Sep 1998 15:58:27 +0200] rev 5516
added indentation
oheimb [Mon, 21 Sep 1998 12:01:14 +0200] rev 5515
simplified proof
paulson [Mon, 21 Sep 1998 10:46:58 +0200] rev 5514
inserted space in #-1 to prevent confusion with an integer constant
paulson [Mon, 21 Sep 1998 10:43:54 +0200] rev 5513
Unary minus is now #- and not #~
paulson [Mon, 21 Sep 1998 10:43:09 +0200] rev 5512
much renaming and tidying
paulson [Fri, 18 Sep 1998 16:07:55 +0200] rev 5511
leaves subgoal package empty
paulson [Fri, 18 Sep 1998 16:05:08 +0200] rev 5510
improved (but still flawed) treatment of binary arithmetic
paulson [Fri, 18 Sep 1998 16:04:44 +0200] rev 5509
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson [Fri, 18 Sep 1998 16:04:00 +0200] rev 5508
new files in Integ