Wed, 02 Oct 2002 15:26:07 +0200 *** empty log message ***
nipkow [Wed, 02 Oct 2002 15:26:07 +0200] rev 13620
*** empty log message ***
Tue, 01 Oct 2002 20:54:17 +0200 *** empty log message ***
nipkow [Tue, 01 Oct 2002 20:54:17 +0200] rev 13619
*** empty log message ***
Tue, 01 Oct 2002 15:03:28 +0200 Added some comments on new simplifier.
berghofe [Tue, 01 Oct 2002 15:03:28 +0200] rev 13618
Added some comments on new simplifier.
Tue, 01 Oct 2002 14:45:28 +0200 Documented new "asm_lr" option for simp.
berghofe [Tue, 01 Oct 2002 14:45:28 +0200] rev 13617
Documented new "asm_lr" option for simp.
Tue, 01 Oct 2002 14:44:43 +0200 Adapted to new simplifier.
berghofe [Tue, 01 Oct 2002 14:44:43 +0200] rev 13616
Adapted to new simplifier.
Tue, 01 Oct 2002 13:26:10 +0200 Numerous cosmetic changes, prompted by the new simplifier
paulson [Tue, 01 Oct 2002 13:26:10 +0200] rev 13615
Numerous cosmetic changes, prompted by the new simplifier
Tue, 01 Oct 2002 11:17:25 +0200 Deleted superfluous dest_implies.
berghofe [Tue, 01 Oct 2002 11:17:25 +0200] rev 13614
Deleted superfluous dest_implies.
Mon, 30 Sep 2002 16:50:39 +0200 *** empty log message ***
nipkow [Mon, 30 Sep 2002 16:50:39 +0200] rev 13613
*** empty log message ***
Mon, 30 Sep 2002 16:48:15 +0200 Adapted to new simplifier.
berghofe [Mon, 30 Sep 2002 16:48:15 +0200] rev 13612
Adapted to new simplifier.
Mon, 30 Sep 2002 16:47:03 +0200 Adapted to new simplifier.
berghofe [Mon, 30 Sep 2002 16:47:03 +0200] rev 13611
Adapted to new simplifier.
Mon, 30 Sep 2002 16:44:00 +0200 Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
berghofe [Mon, 30 Sep 2002 16:44:00 +0200] rev 13610
Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
Mon, 30 Sep 2002 16:42:46 +0200 Added check for axioms with "realizes Null A = A".
berghofe [Mon, 30 Sep 2002 16:42:46 +0200] rev 13609
Added check for axioms with "realizes Null A = A".
Mon, 30 Sep 2002 16:40:57 +0200 Added function elim_vars.
berghofe [Mon, 30 Sep 2002 16:40:57 +0200] rev 13608
Added function elim_vars.
Mon, 30 Sep 2002 16:38:22 +0200 Completely reimplemented mutual simplification of premises.
berghofe [Mon, 30 Sep 2002 16:38:22 +0200] rev 13607
Completely reimplemented mutual simplification of premises.
Mon, 30 Sep 2002 16:37:44 +0200 Removed nRS again because extract_rews now takes care of preserving names.
berghofe [Mon, 30 Sep 2002 16:37:44 +0200] rev 13606
Removed nRS again because extract_rews now takes care of preserving names.
Mon, 30 Sep 2002 16:36:57 +0200 Added syntax for "asm_lr" simplifier option.
berghofe [Mon, 30 Sep 2002 16:36:57 +0200] rev 13605
Added syntax for "asm_lr" simplifier option.
Mon, 30 Sep 2002 16:34:56 +0200 - eliminated thin_leading_eqs_tac
berghofe [Mon, 30 Sep 2002 16:34:56 +0200] rev 13604
- eliminated thin_leading_eqs_tac - gen_hyp_subst_tac now uses asm_lr_simp_tac instead of asm_full_simp_tac, in order to avoid divergence of new simplifier
Mon, 30 Sep 2002 16:32:05 +0200 Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
berghofe [Mon, 30 Sep 2002 16:32:05 +0200] rev 13603
Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
Mon, 30 Sep 2002 16:27:38 +0200 - additional congruence rules for boolean operators
berghofe [Mon, 30 Sep 2002 16:27:38 +0200] rev 13602
- additional congruence rules for boolean operators - additional rewrite rules for exI / exE
Mon, 30 Sep 2002 16:14:02 +0200 Adapted to new simplifier.
berghofe [Mon, 30 Sep 2002 16:14:02 +0200] rev 13601
Adapted to new simplifier.
Mon, 30 Sep 2002 16:12:16 +0200 Removed nRS again because extract_rews now takes care of preserving names.
berghofe [Mon, 30 Sep 2002 16:12:16 +0200] rev 13600
Removed nRS again because extract_rews now takes care of preserving names.
Mon, 30 Sep 2002 16:10:32 +0200 Added elim_vars to preprocessor.
berghofe [Mon, 30 Sep 2002 16:10:32 +0200] rev 13599
Added elim_vars to preprocessor.
Mon, 30 Sep 2002 16:09:05 +0200 Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe [Mon, 30 Sep 2002 16:09:05 +0200] rev 13598
Fixed problem with induct_conj_curry: variable C should have type prop.
Mon, 30 Sep 2002 15:45:11 +0200 fixes !!-bound vars in induction statement automatically
nipkow [Mon, 30 Sep 2002 15:45:11 +0200] rev 13597
fixes !!-bound vars in induction statement automatically
Mon, 30 Sep 2002 15:44:21 +0200 modified induct method
nipkow [Mon, 30 Sep 2002 15:44:21 +0200] rev 13596
modified induct method
Fri, 27 Sep 2002 16:44:50 +0200 Proof tidying
paulson [Fri, 27 Sep 2002 16:44:50 +0200] rev 13595
Proof tidying
Fri, 27 Sep 2002 13:24:29 +0200 Isar experiments, etc.
paulson [Fri, 27 Sep 2002 13:24:29 +0200] rev 13594
Isar experiments, etc.
Fri, 27 Sep 2002 10:36:21 +0200 Tidied. New Pi-theorem.
paulson [Fri, 27 Sep 2002 10:36:21 +0200] rev 13593
Tidied. New Pi-theorem.
Fri, 27 Sep 2002 10:35:10 +0200 new Ring example
paulson [Fri, 27 Sep 2002 10:35:10 +0200] rev 13592
new Ring example
Fri, 27 Sep 2002 10:35:01 +0200 Isar proof
paulson [Fri, 27 Sep 2002 10:35:01 +0200] rev 13591
Isar proof
Fri, 27 Sep 2002 10:34:05 +0200 Modules theory added
paulson [Fri, 27 Sep 2002 10:34:05 +0200] rev 13590
Modules theory added
Fri, 27 Sep 2002 10:33:47 +0200 New theory GroupTheory/Module.thy of modules
paulson [Fri, 27 Sep 2002 10:33:47 +0200] rev 13589
New theory GroupTheory/Module.thy of modules
Thu, 26 Sep 2002 15:21:38 +0200 Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson [Thu, 26 Sep 2002 15:21:38 +0200] rev 13588
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML (which is automatically loaded with Int.thy) on case-insensitive filesystems.
Thu, 26 Sep 2002 10:56:20 +0200 GroupTheory and FuncSet
paulson [Thu, 26 Sep 2002 10:56:20 +0200] rev 13587
GroupTheory and FuncSet
Thu, 26 Sep 2002 10:51:58 +0200 new theory for Pi-sets, restrict, etc.
paulson [Thu, 26 Sep 2002 10:51:58 +0200] rev 13586
new theory for Pi-sets, restrict, etc.
Thu, 26 Sep 2002 10:51:29 +0200 Converted Fun to Isar style.
paulson [Thu, 26 Sep 2002 10:51:29 +0200] rev 13585
Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
Thu, 26 Sep 2002 10:43:43 +0200 new document directory for GroupTheory
paulson [Thu, 26 Sep 2002 10:43:43 +0200] rev 13584
new document directory for GroupTheory
Thu, 26 Sep 2002 10:40:13 +0200 converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson [Thu, 26 Sep 2002 10:40:13 +0200] rev 13583
converted to Isar and using new "implicit structures" instead of Sigma, etc
Wed, 25 Sep 2002 11:23:26 +0200 *** empty log message ***
nipkow [Wed, 25 Sep 2002 11:23:26 +0200] rev 13582
*** empty log message ***
Wed, 25 Sep 2002 11:22:28 +0200 *** empty log message ***
nipkow [Wed, 25 Sep 2002 11:22:28 +0200] rev 13581
*** empty log message ***
Wed, 25 Sep 2002 11:06:34 +0200 *** empty log message ***
nipkow [Wed, 25 Sep 2002 11:06:34 +0200] rev 13580
*** empty log message ***
Wed, 25 Sep 2002 07:57:36 +0200 Int.thy -> int.thy
nipkow [Wed, 25 Sep 2002 07:57:36 +0200] rev 13579
Int.thy -> int.thy
Wed, 25 Sep 2002 07:55:56 +0200 became int.ML
nipkow [Wed, 25 Sep 2002 07:55:56 +0200] rev 13578
became int.ML
Wed, 25 Sep 2002 07:54:33 +0200 conversion to Isar
nipkow [Wed, 25 Sep 2002 07:54:33 +0200] rev 13577
conversion to Isar
Wed, 25 Sep 2002 07:52:07 +0200 converted to Isar
nipkow [Wed, 25 Sep 2002 07:52:07 +0200] rev 13576
converted to Isar
Wed, 25 Sep 2002 07:42:24 +0200 added nat_split
nipkow [Wed, 25 Sep 2002 07:42:24 +0200] rev 13575
added nat_split
Sat, 21 Sep 2002 21:10:34 +0200 converted to Isar script
paulson [Sat, 21 Sep 2002 21:10:34 +0200] rev 13574
converted to Isar script
Fri, 20 Sep 2002 11:49:38 +0200 shortened a proof
paulson [Fri, 20 Sep 2002 11:49:38 +0200] rev 13573
shortened a proof
Fri, 20 Sep 2002 11:49:06 +0200 got rid of deepen_tac
paulson [Fri, 20 Sep 2002 11:49:06 +0200] rev 13572
got rid of deepen_tac
Fri, 20 Sep 2002 11:48:35 +0200 less use of x-symbols
paulson [Fri, 20 Sep 2002 11:48:35 +0200] rev 13571
less use of x-symbols
Thu, 19 Sep 2002 16:09:16 +0200 *** empty log message ***
nipkow [Thu, 19 Sep 2002 16:09:16 +0200] rev 13570
*** empty log message ***
Thu, 19 Sep 2002 16:01:29 +0200 drule: added nRS
nipkow [Thu, 19 Sep 2002 16:01:29 +0200] rev 13569
drule: added nRS simplifier: trace with names
Thu, 19 Sep 2002 16:00:27 +0200 preserve names of rewrite rules when transforming them
nipkow [Thu, 19 Sep 2002 16:00:27 +0200] rev 13568
preserve names of rewrite rules when transforming them
Wed, 18 Sep 2002 18:19:43 +0200 comments + usage
kleing [Wed, 18 Sep 2002 18:19:43 +0200] rev 13567
comments + usage
Wed, 11 Sep 2002 16:55:37 +0200 Streamlined proofs of instances of Separation
paulson [Wed, 11 Sep 2002 16:55:37 +0200] rev 13566
Streamlined proofs of instances of Separation
Wed, 11 Sep 2002 16:53:59 +0200 Bound variable preservation in Collect_cong
paulson [Wed, 11 Sep 2002 16:53:59 +0200] rev 13565
Bound variable preservation in Collect_cong
Tue, 10 Sep 2002 16:51:31 +0200 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson [Tue, 10 Sep 2002 16:51:31 +0200] rev 13564
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
Tue, 10 Sep 2002 16:47:17 +0200 tweaks
paulson [Tue, 10 Sep 2002 16:47:17 +0200] rev 13563
tweaks
Mon, 09 Sep 2002 17:28:29 +0200 *** empty log message ***
nipkow [Mon, 09 Sep 2002 17:28:29 +0200] rev 13562
*** empty log message ***
Mon, 09 Sep 2002 17:07:12 +0200 bug in counter example finder
nipkow [Mon, 09 Sep 2002 17:07:12 +0200] rev 13561
bug in counter example finder
Sat, 07 Sep 2002 22:04:28 +0200 conversion of ZF/Integ/{Int,Bin} to Isar scripts
paulson [Sat, 07 Sep 2002 22:04:28 +0200] rev 13560
conversion of ZF/Integ/{Int,Bin} to Isar scripts
Thu, 05 Sep 2002 14:03:03 +0200 added checking so that (rename_tac "x y") is rejected, since
paulson [Thu, 05 Sep 2002 14:03:03 +0200] rev 13559
added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier
Tue, 03 Sep 2002 18:49:30 +0200 tidied
paulson [Tue, 03 Sep 2002 18:49:30 +0200] rev 13558
tidied
Tue, 03 Sep 2002 18:49:10 +0200 deleted redundant material (quasiformula, ...) and rationalized
paulson [Tue, 03 Sep 2002 18:49:10 +0200] rev 13557
deleted redundant material (quasiformula, ...) and rationalized
Tue, 03 Sep 2002 18:43:15 +0200 fixed the typesetting
paulson [Tue, 03 Sep 2002 18:43:15 +0200] rev 13556
fixed the typesetting
Tue, 03 Sep 2002 13:41:29 +0200 *** empty log message ***
nipkow [Tue, 03 Sep 2002 13:41:29 +0200] rev 13555
*** empty log message ***
Mon, 02 Sep 2002 12:25:19 +0200 Added missing rewrite rule and some arith examples
paulson [Mon, 02 Sep 2002 12:25:19 +0200] rev 13554
Added missing rewrite rule and some arith examples
Mon, 02 Sep 2002 11:07:26 +0200 order_less_irrefl: [simp] -> [iff]
nipkow [Mon, 02 Sep 2002 11:07:26 +0200] rev 13553
order_less_irrefl: [simp] -> [iff]
Sun, 01 Sep 2002 19:39:25 +0200 *** empty log message ***
nipkow [Sun, 01 Sep 2002 19:39:25 +0200] rev 13552
*** empty log message ***
Sat, 31 Aug 2002 14:03:49 +0200 converted Hyperreal/Zorn to Isar format and moved to Library
paulson [Sat, 31 Aug 2002 14:03:49 +0200] rev 13551
converted Hyperreal/Zorn to Isar format and moved to Library
Fri, 30 Aug 2002 16:42:45 +0200 removal of blast.overloaded
paulson [Fri, 30 Aug 2002 16:42:45 +0200] rev 13550
removal of blast.overloaded
Thu, 29 Aug 2002 16:15:11 +0200 updated;
wenzelm [Thu, 29 Aug 2002 16:15:11 +0200] rev 13549
updated;
Thu, 29 Aug 2002 16:08:32 +0200 *** empty log message ***
wenzelm [Thu, 29 Aug 2002 16:08:32 +0200] rev 13548
*** empty log message ***
Thu, 29 Aug 2002 16:08:30 +0200 tuned;
wenzelm [Thu, 29 Aug 2002 16:08:30 +0200] rev 13547
tuned;
Thu, 29 Aug 2002 11:15:36 +0200 fixed a name clash
paulson [Thu, 29 Aug 2002 11:15:36 +0200] rev 13546
fixed a name clash
Wed, 28 Aug 2002 15:27:43 +0200 improved tell_thm_deps;
wenzelm [Wed, 28 Aug 2002 15:27:43 +0200] rev 13545
improved tell_thm_deps;
Wed, 28 Aug 2002 13:08:50 +0200 various new lemmas for Constructible
paulson [Wed, 28 Aug 2002 13:08:50 +0200] rev 13544
various new lemmas for Constructible
Wed, 28 Aug 2002 13:08:34 +0200 completion of the consistency proof for AC
paulson [Wed, 28 Aug 2002 13:08:34 +0200] rev 13543
completion of the consistency proof for AC
Tue, 27 Aug 2002 17:25:44 +0200 thms_containing: allow "_" in specification;
wenzelm [Tue, 27 Aug 2002 17:25:44 +0200] rev 13542
thms_containing: allow "_" in specification;
Tue, 27 Aug 2002 17:24:41 +0200 *** empty log message ***
wenzelm [Tue, 27 Aug 2002 17:24:41 +0200] rev 13541
*** empty log message ***
Tue, 27 Aug 2002 16:41:52 +0200 * Pure: disallow duplicate fact bindings within new-style theory files;
wenzelm [Tue, 27 Aug 2002 16:41:52 +0200] rev 13540
* Pure: disallow duplicate fact bindings within new-style theory files;
Tue, 27 Aug 2002 16:41:01 +0200 disallow duplicate fact bindings for drafts (i.e. within new-style theory files);
wenzelm [Tue, 27 Aug 2002 16:41:01 +0200] rev 13539
disallow duplicate fact bindings for drafts (i.e. within new-style theory files);
Tue, 27 Aug 2002 15:40:58 +0200 tuned;
wenzelm [Tue, 27 Aug 2002 15:40:58 +0200] rev 13538
tuned;
Tue, 27 Aug 2002 15:40:33 +0200 avoid duplicate fact bindings;
wenzelm [Tue, 27 Aug 2002 15:40:33 +0200] rev 13537
avoid duplicate fact bindings;
Tue, 27 Aug 2002 15:39:39 +0200 removed IsarTut;
wenzelm [Tue, 27 Aug 2002 15:39:39 +0200] rev 13536
removed IsarTut;
Tue, 27 Aug 2002 11:09:35 +0200 *** empty log message ***
wenzelm [Tue, 27 Aug 2002 11:09:35 +0200] rev 13535
*** empty log message ***
Tue, 27 Aug 2002 11:09:33 +0200 avoid duplicate fact bindings;
wenzelm [Tue, 27 Aug 2002 11:09:33 +0200] rev 13534
avoid duplicate fact bindings;
Tue, 27 Aug 2002 11:07:54 +0200 check_file: disallow current dir (typically "");
wenzelm [Tue, 27 Aug 2002 11:07:54 +0200] rev 13533
check_file: disallow current dir (typically "");
Tue, 27 Aug 2002 11:07:01 +0200 simplified results;
wenzelm [Tue, 27 Aug 2002 11:07:01 +0200] rev 13532
simplified results; added hook;
Tue, 27 Aug 2002 11:06:45 +0200 simplified results;
wenzelm [Tue, 27 Aug 2002 11:06:45 +0200] rev 13531
simplified results;
Tue, 27 Aug 2002 11:06:20 +0200 Thm.proof_of;
wenzelm [Tue, 27 Aug 2002 11:06:20 +0200] rev 13530
Thm.proof_of;
Tue, 27 Aug 2002 11:06:07 +0200 check_goal: produce error instead of warning;
wenzelm [Tue, 27 Aug 2002 11:06:07 +0200] rev 13529
check_goal: produce error instead of warning;
Tue, 27 Aug 2002 11:05:31 +0200 added proof_of;
wenzelm [Tue, 27 Aug 2002 11:05:31 +0200] rev 13528
added proof_of;
Tue, 27 Aug 2002 11:05:13 +0200 thms/axms_of_proof: proper handling of MinProof;
wenzelm [Tue, 27 Aug 2002 11:05:13 +0200] rev 13527
thms/axms_of_proof: proper handling of MinProof;
Tue, 27 Aug 2002 11:04:27 +0200 result dependency output;
wenzelm [Tue, 27 Aug 2002 11:04:27 +0200] rev 13526
result dependency output;
Tue, 27 Aug 2002 11:04:00 +0200 dup_elim: improved error reporting;
wenzelm [Tue, 27 Aug 2002 11:04:00 +0200] rev 13525
dup_elim: improved error reporting;
Tue, 27 Aug 2002 11:03:05 +0200 *** empty log message ***
wenzelm [Tue, 27 Aug 2002 11:03:05 +0200] rev 13524
*** empty log message ***
Tue, 27 Aug 2002 11:03:02 +0200 avoid duplicate fact bindings;
wenzelm [Tue, 27 Aug 2002 11:03:02 +0200] rev 13523
avoid duplicate fact bindings;
Tue, 27 Aug 2002 10:59:21 +0200 * Isar: preview of problems to finish 'show' now produce an error
wenzelm [Tue, 27 Aug 2002 10:59:21 +0200] rev 13522
* Isar: preview of problems to finish 'show' now produce an error
Sat, 24 Aug 2002 18:53:43 +0200 conversion of ZF/IntDiv to Isar script
paulson [Sat, 24 Aug 2002 18:53:43 +0200] rev 13521
conversion of ZF/IntDiv to Isar script
Sat, 24 Aug 2002 18:45:21 +0200 conversion of ZF/IntDiv to Isar script
paulson [Sat, 24 Aug 2002 18:45:21 +0200] rev 13520
conversion of ZF/IntDiv to Isar script
Fri, 23 Aug 2002 17:10:47 +0200 *** empty log message ***
nipkow [Fri, 23 Aug 2002 17:10:47 +0200] rev 13519
*** empty log message ***
Fri, 23 Aug 2002 11:08:01 +0200 *** empty log message ***
nipkow [Fri, 23 Aug 2002 11:08:01 +0200] rev 13518
*** empty log message ***
Fri, 23 Aug 2002 07:41:05 +0200 Added div+mod cancelling simproc
nipkow [Fri, 23 Aug 2002 07:41:05 +0200] rev 13517
Added div+mod cancelling simproc
Fri, 23 Aug 2002 07:34:20 +0200 for cancelling div + mod.
nipkow [Fri, 23 Aug 2002 07:34:20 +0200] rev 13516
for cancelling div + mod.
Thu, 22 Aug 2002 20:49:43 +0200 updated to use locales (still some rough edges);
wenzelm [Thu, 22 Aug 2002 20:49:43 +0200] rev 13515
updated to use locales (still some rough edges);
Thu, 22 Aug 2002 12:28:41 +0200 tweaked
paulson [Thu, 22 Aug 2002 12:28:41 +0200] rev 13514
tweaked
Wed, 21 Aug 2002 15:57:24 +0200 tweaks
paulson [Wed, 21 Aug 2002 15:57:24 +0200] rev 13513
tweaks
Wed, 21 Aug 2002 15:57:08 +0200 tweaks and new lemmas
paulson [Wed, 21 Aug 2002 15:57:08 +0200] rev 13512
tweaks and new lemmas
Wed, 21 Aug 2002 15:56:37 +0200 new proof needed now
paulson [Wed, 21 Aug 2002 15:56:37 +0200] rev 13511
new proof needed now
Wed, 21 Aug 2002 15:55:59 +0200 proof can be shortened now
paulson [Wed, 21 Aug 2002 15:55:59 +0200] rev 13510
proof can be shortened now
Wed, 21 Aug 2002 15:55:40 +0200 new lemmas
paulson [Wed, 21 Aug 2002 15:55:40 +0200] rev 13509
new lemmas
Wed, 21 Aug 2002 15:53:30 +0200 Frederic Blanqui's new "guard" examples
paulson [Wed, 21 Aug 2002 15:53:30 +0200] rev 13508
Frederic Blanqui's new "guard" examples
Sat, 17 Aug 2002 14:55:08 +0200 tidying of Isar scripts
paulson [Sat, 17 Aug 2002 14:55:08 +0200] rev 13507
tidying of Isar scripts
Fri, 16 Aug 2002 17:19:43 +0200 Various tweaks of the presentation
paulson [Fri, 16 Aug 2002 17:19:43 +0200] rev 13506
Various tweaks of the presentation
Fri, 16 Aug 2002 16:41:48 +0200 Relativized right up to L satisfies V=L!
paulson [Fri, 16 Aug 2002 16:41:48 +0200] rev 13505
Relativized right up to L satisfies V=L!
Fri, 16 Aug 2002 12:48:49 +0200 Tidying up
paulson [Fri, 16 Aug 2002 12:48:49 +0200] rev 13504
Tidying up
Thu, 15 Aug 2002 21:36:26 +0200 Relativization and absoluteness for DPow!!
paulson [Thu, 15 Aug 2002 21:36:26 +0200] rev 13503
Relativization and absoluteness for DPow!!
Wed, 14 Aug 2002 14:33:26 +0200 Finished absoluteness of "satisfies"!!
paulson [Wed, 14 Aug 2002 14:33:26 +0200] rev 13502
Finished absoluteness of "satisfies"!!
Tue, 13 Aug 2002 22:01:53 +0200 arith_tac should not produce counter example
nipkow [Tue, 13 Aug 2002 22:01:53 +0200] rev 13501
arith_tac should not produce counter example
(0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip