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