Thu, 24 Jul 2003 18:23:00 +0200 declarations moved from PreList.thy
paulson [Thu, 24 Jul 2003 18:23:00 +0200] rev 14131
declarations moved from PreList.thy
Thu, 24 Jul 2003 17:52:38 +0200 Fixed two bugs:
berghofe [Thu, 24 Jul 2003 17:52:38 +0200] rev 14130
Fixed two bugs: - presburger_tac now calls ObjectLogic.atomize_tac first to avoid failure when premises contain meta-level quantifiers or implications - The preprocessor now also filters out premises containing variables that are not of type int or nat.
Thu, 24 Jul 2003 17:47:56 +0200 Exported function get_mode.
berghofe [Thu, 24 Jul 2003 17:47:56 +0200] rev 14129
Exported function get_mode.
Thu, 24 Jul 2003 16:41:40 +0200 header comment
paulson [Thu, 24 Jul 2003 16:41:40 +0200] rev 14128
header comment
Thu, 24 Jul 2003 16:37:04 +0200 new theory NatPair of the injection from nat*nat -> nat
paulson [Thu, 24 Jul 2003 16:37:04 +0200] rev 14127
new theory NatPair of the injection from nat*nat -> nat
Thu, 24 Jul 2003 16:36:29 +0200 Tidying and replacement of some axioms by specifications
paulson [Thu, 24 Jul 2003 16:36:29 +0200] rev 14126
Tidying and replacement of some axioms by specifications
Thu, 24 Jul 2003 16:35:51 +0200 tidied
paulson [Thu, 24 Jul 2003 16:35:51 +0200] rev 14125
tidied
Tue, 22 Jul 2003 11:05:02 +0200 Added some regression testing for simprocs
paulson [Tue, 22 Jul 2003 11:05:02 +0200] rev 14124
Added some regression testing for simprocs
Tue, 22 Jul 2003 11:03:42 +0200 fixed simprocs
paulson [Tue, 22 Jul 2003 11:03:42 +0200] rev 14123
fixed simprocs
Mon, 21 Jul 2003 17:27:23 +0200 Added handling of meta implication and meta quantification.
skalberg [Mon, 21 Jul 2003 17:27:23 +0200] rev 14122
Added handling of meta implication and meta quantification.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip