nipkow [Tue, 04 Sep 2001 17:31:18 +0200] rev 11548
*** empty log message ***
nipkow [Mon, 03 Sep 2001 10:28:52 +0200] rev 11547
*** empty log message ***
wenzelm [Sat, 01 Sep 2001 00:20:44 +0200] rev 11546
tuned;
wenzelm [Sat, 01 Sep 2001 00:20:22 +0200] rev 11545
final proofs := 0;
wenzelm [Sat, 01 Sep 2001 00:20:06 +0200] rev 11544
HOL-Real-Hyperreal made a plain session (no longer an image);
wenzelm [Sat, 01 Sep 2001 00:14:16 +0200] rev 11543
renamed `keep_derivs' to `proofs', and made an integer;
wenzelm [Fri, 31 Aug 2001 22:46:23 +0200] rev 11542
* Proof General keywords specification is now part of the Isabelle
distribution (see etc/isar-keywords.el);
wenzelm [Fri, 31 Aug 2001 22:45:08 +0200] rev 11541
proper use of invent_names;
wenzelm [Fri, 31 Aug 2001 22:44:44 +0200] rev 11540
fixed header;
wenzelm [Fri, 31 Aug 2001 18:46:48 +0200] rev 11539
tuned headers;
wenzelm [Fri, 31 Aug 2001 18:43:27 +0200] rev 11538
keyword classification tables for Isabelle/Isar Proof General
(generated by ProofGeneral.write_keywords from Isabelle/HOLCF/IOA);
berghofe [Fri, 31 Aug 2001 16:49:06 +0200] rev 11537
New code generators for HOL.
berghofe [Fri, 31 Aug 2001 16:45:47 +0200] rev 11536
Initial revision of tools for proof terms.
berghofe [Fri, 31 Aug 2001 16:30:31 +0200] rev 11535
Added new option for setting level of detail for proof objects.
berghofe [Fri, 31 Aug 2001 16:29:18 +0200] rev 11534
Proof of True_implies_equals is stored with "open" derivation to
facilitate simplification of proof terms.
berghofe [Fri, 31 Aug 2001 16:28:26 +0200] rev 11533
Added code generator setup.
berghofe [Fri, 31 Aug 2001 16:27:43 +0200] rev 11532
Added new files for code generator.
berghofe [Fri, 31 Aug 2001 16:26:55 +0200] rev 11531
Renamed functions % and %% to avoid clash with syntax for proof terms.
berghofe [Fri, 31 Aug 2001 16:25:53 +0200] rev 11530
Adapted to new proof terms.
berghofe [Fri, 31 Aug 2001 16:24:39 +0200] rev 11529
Exported ml_reserved.
berghofe [Fri, 31 Aug 2001 16:24:00 +0200] rev 11528
Made consts list operations a bit faster.
berghofe [Fri, 31 Aug 2001 16:22:48 +0200] rev 11527
Added new argument to use_dir for derivation kind.
berghofe [Fri, 31 Aug 2001 16:22:02 +0200] rev 11526
Removed tag_assumption.
berghofe [Fri, 31 Aug 2001 16:21:31 +0200] rev 11525
Tuned naming of theorems.
berghofe [Fri, 31 Aug 2001 16:20:19 +0200] rev 11524
Added functions for printing primitive proof terms.
berghofe [Fri, 31 Aug 2001 16:17:52 +0200] rev 11523
Tuned function extend_lexicon.
berghofe [Fri, 31 Aug 2001 16:17:05 +0200] rev 11522
Initial revision of tools for proof terms.
berghofe [Fri, 31 Aug 2001 16:15:36 +0200] rev 11521
Now obsolete; replaced by LF style proof terms.
berghofe [Fri, 31 Aug 2001 16:14:34 +0200] rev 11520
Initial version of generic code generator.
berghofe [Fri, 31 Aug 2001 16:13:36 +0200] rev 11519
New implementation of LF style proof terms.
berghofe [Fri, 31 Aug 2001 16:13:00 +0200] rev 11518
Replaced old derivations by proof terms.
berghofe [Fri, 31 Aug 2001 16:12:15 +0200] rev 11517
Tidied function SELECT_GOAL.
berghofe [Fri, 31 Aug 2001 16:11:20 +0200] rev 11516
Added equality axioms and initialization of proof term package.
berghofe [Fri, 31 Aug 2001 16:10:03 +0200] rev 11515
Added setup for code generator.
berghofe [Fri, 31 Aug 2001 16:09:25 +0200] rev 11514
Added function unique_strings.
berghofe [Fri, 31 Aug 2001 16:08:45 +0200] rev 11513
- exported SAME exception
- exported functions for normalizing types
berghofe [Fri, 31 Aug 2001 16:07:56 +0200] rev 11512
Some basic rules are now stored with "open" derivations, to facilitate
simplification of proof terms.
berghofe [Fri, 31 Aug 2001 16:06:21 +0200] rev 11511
Added new files for proof terms.
wenzelm [Thu, 30 Aug 2001 22:51:11 +0200] rev 11510
generated by Session.name;
wenzelm [Thu, 30 Aug 2001 22:50:01 +0200] rev 11509
export name;
oheimb [Thu, 30 Aug 2001 17:49:46 +0200] rev 11508
cosmetics
oheimb [Thu, 30 Aug 2001 15:47:30 +0200] rev 11507
removed imname, uncurried Meth
wenzelm [Wed, 29 Aug 2001 21:17:24 +0200] rev 11506
avoid ML bindings;
nipkow [Tue, 28 Aug 2001 14:25:26 +0200] rev 11505
Implemented indentation schema for conditional rewrite trace.
nipkow [Thu, 23 Aug 2001 14:32:48 +0200] rev 11504
Traced depth of conditional rewriting
wenzelm [Tue, 21 Aug 2001 20:09:09 +0200] rev 11503
tuned error message;
wenzelm [Thu, 16 Aug 2001 23:19:12 +0200] rev 11502
prefer immediate monos;
tuned;
wenzelm [Wed, 15 Aug 2001 22:20:30 +0200] rev 11501
support for absolute namespace entry paths;
paulson [Fri, 10 Aug 2001 10:25:45 +0200] rev 11500
Updated proofs to take advantage of additional theorems proved by "typedef"
wenzelm [Thu, 09 Aug 2001 23:42:45 +0200] rev 11499
removed obsolete "arities";
wenzelm [Thu, 09 Aug 2001 22:07:39 +0200] rev 11498
tuned;
oheimb [Thu, 09 Aug 2001 20:48:57 +0200] rev 11497
corrected initialization of locals, streamlined Impl
oheimb [Thu, 09 Aug 2001 19:33:22 +0200] rev 11496
corrected semantics of [iff] concerning rules with premises
oheimb [Thu, 09 Aug 2001 18:51:41 +0200] rev 11495
replaced 1 by 1'
paulson [Thu, 09 Aug 2001 18:12:15 +0200] rev 11494
revisions and indexing
oheimb [Thu, 09 Aug 2001 10:17:45 +0200] rev 11493
added pair_imageI (also as intro rule)
oheimb [Thu, 09 Aug 2001 10:16:23 +0200] rev 11492
renamed addaltern to addafter, addSaltern to addSafter
wenzelm [Wed, 08 Aug 2001 17:39:32 +0200] rev 11491
added constify_ast_tr;
wenzelm [Wed, 08 Aug 2001 17:39:16 +0200] rev 11490
field_name_ast_tr superceded by constify_ast_tr in Pure;
wenzelm [Wed, 08 Aug 2001 17:38:53 +0200] rev 11489
_constify;
wenzelm [Wed, 08 Aug 2001 17:38:29 +0200] rev 11488
constify numeral tokens in order to allow translations;
wenzelm [Wed, 08 Aug 2001 17:37:47 +0200] rev 11487
* HOL: syntax translations now work properly with numerals and records
expressions;
oheimb [Wed, 08 Aug 2001 16:57:43 +0200] rev 11486
layout, subscripts
wenzelm [Wed, 08 Aug 2001 15:16:38 +0200] rev 11485
[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";
wenzelm [Wed, 08 Aug 2001 14:57:22 +0200] rev 11484
polyml-4.1.1;
paulson [Wed, 08 Aug 2001 14:52:10 +0200] rev 11483
Hilbert_Choice is needed only in Main itself
paulson [Wed, 08 Aug 2001 14:51:30 +0200] rev 11482
Main is the proper parent of IOA
paulson [Wed, 08 Aug 2001 14:51:10 +0200] rev 11481
get it working again using Hilbert_Choice
paulson [Wed, 08 Aug 2001 14:50:28 +0200] rev 11480
Getting it working again with 1' instead of 1
paulson [Wed, 08 Aug 2001 14:33:10 +0200] rev 11479
new ZF/UNITY theory
wenzelm [Wed, 08 Aug 2001 14:16:42 +0200] rev 11478
*** empty log message ***
oheimb [Wed, 08 Aug 2001 14:12:36 +0200] rev 11477
changed to full expressions with side effects
oheimb [Wed, 08 Aug 2001 12:36:48 +0200] rev 11476
changed to full expressions with side effects
wenzelm [Tue, 07 Aug 2001 22:42:22 +0200] rev 11475
tuned;
wenzelm [Tue, 07 Aug 2001 22:41:46 +0200] rev 11474
tuned;
wenzelm [Tue, 07 Aug 2001 22:37:30 +0200] rev 11473
fix problem with user translations by making field names appear as consts;
wenzelm [Tue, 07 Aug 2001 21:27:00 +0200] rev 11472
tuned;
berghofe [Tue, 07 Aug 2001 19:29:08 +0200] rev 11471
- Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
- Funs_rangeE now requires function g to be injective
berghofe [Tue, 07 Aug 2001 19:26:42 +0200] rev 11470
Eliminated dependency of Funs_rangeE on SOME.
oheimb [Tue, 07 Aug 2001 17:21:58 +0200] rev 11469
removed the warning from [iff]
paulson [Tue, 07 Aug 2001 16:36:52 +0200] rev 11468
Tweaks for 1 -> 1'
paulson [Mon, 06 Aug 2001 16:43:40 +0200] rev 11467
Converted 1 to 1'
nipkow [Mon, 06 Aug 2001 15:54:29 +0200] rev 11466
1 -> 1'
paulson [Mon, 06 Aug 2001 15:46:20 +0200] rev 11465
Changed 1 to 1' (= Suc 0)
nipkow [Mon, 06 Aug 2001 13:43:24 +0200] rev 11464
turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.
paulson [Mon, 06 Aug 2001 13:12:06 +0200] rev 11463
three new theorems
paulson [Mon, 06 Aug 2001 12:46:21 +0200] rev 11462
removed the warning from [iff]
paulson [Mon, 06 Aug 2001 12:42:43 +0200] rev 11461
removed an unsuitable default simprule
paulson [Mon, 06 Aug 2001 12:41:21 +0200] rev 11460
tidying and moving the theorem "choice"
paulson [Mon, 06 Aug 2001 12:40:39 +0200] rev 11459
new result comp_surj
paulson [Fri, 03 Aug 2001 18:04:55 +0200] rev 11458
numerous stylistic changes and indexing
paulson [Thu, 26 Jul 2001 18:23:38 +0200] rev 11457
additional revisions to chapters 1, 2
paulson [Thu, 26 Jul 2001 16:43:02 +0200] rev 11456
revisions and indexing
paulson [Wed, 25 Jul 2001 18:21:01 +0200] rev 11455
defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some
dynamically, so recdef no longer needs to import Hilbert_Choice.
paulson [Wed, 25 Jul 2001 17:58:26 +0200] rev 11454
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson [Wed, 25 Jul 2001 13:44:32 +0200] rev 11453
partial restructuring to reduce dependence on Axiom of Choice
paulson [Wed, 25 Jul 2001 13:33:08 +0200] rev 11452
removed reference to Ex_def
paulson [Wed, 25 Jul 2001 13:13:01 +0200] rev 11451
partial restructuring to reduce dependence on Axiom of Choice
paulson [Tue, 24 Jul 2001 11:25:54 +0200] rev 11450
tweaks and indexing
oheimb [Mon, 23 Jul 2001 19:06:11 +0200] rev 11449
cosmetics
paulson [Mon, 23 Jul 2001 17:47:49 +0200] rev 11448
Final version of Florian Kammueller's examples
paulson [Mon, 23 Jul 2001 17:46:40 +0200] rev 11447
new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
paulson [Mon, 23 Jul 2001 17:45:54 +0200] rev 11446
improved version of the Pi-theorems
paulson [Mon, 23 Jul 2001 17:45:35 +0200] rev 11445
PiSets moved to GroupTheory, while LocaleGroup deleted
paulson [Mon, 23 Jul 2001 17:45:07 +0200] rev 11444
live links
paulson [Mon, 23 Jul 2001 17:37:29 +0200] rev 11443
The final version of Florian Kammueller's proofs
oheimb [Mon, 23 Jul 2001 13:50:23 +0200] rev 11442
slight improvement for iff attribute
wenzelm [Sun, 22 Jul 2001 21:31:37 +0200] rev 11441
replaced SOME by THE;
wenzelm [Sun, 22 Jul 2001 21:31:00 +0200] rev 11440
the_equality [intro];
wenzelm [Sun, 22 Jul 2001 21:30:21 +0200] rev 11439
tuned;
wenzelm [Sun, 22 Jul 2001 21:30:05 +0200] rev 11438
declare trans [trans] (*overridden in theory Calculation*);
wenzelm [Fri, 20 Jul 2001 22:02:45 +0200] rev 11437
HOL: added "The";
wenzelm [Fri, 20 Jul 2001 22:00:06 +0200] rev 11436
private "myinv" (uses "The" instead of "Eps");
wenzelm [Fri, 20 Jul 2001 21:59:11 +0200] rev 11435
replaced "Eps" by "The";
wenzelm [Fri, 20 Jul 2001 21:58:19 +0200] rev 11434
HOL_ss: the_eq_trivial, the_sym_eq_trivial;
wenzelm [Fri, 20 Jul 2001 21:53:27 +0200] rev 11433
tuned;
wenzelm [Fri, 20 Jul 2001 21:52:54 +0200] rev 11432
added "The" (definite description operator) (by Larry);
wenzelm [Fri, 20 Jul 2001 17:49:21 +0200] rev 11431
*** empty log message ***
wenzelm [Fri, 20 Jul 2001 17:49:10 +0200] rev 11430
SEDINDEX = ./isa-index;
paulson [Tue, 17 Jul 2001 15:07:36 +0200] rev 11429
tidying the index
paulson [Tue, 17 Jul 2001 13:46:21 +0200] rev 11428
tidying the index
paulson [Mon, 16 Jul 2001 13:14:19 +0200] rev 11427
indexing
wenzelm [Sun, 15 Jul 2001 14:48:36 +0200] rev 11426
abtract non-emptiness statements (no longer use Eps);
cleaned up;
wenzelm [Sun, 15 Jul 2001 14:47:28 +0200] rev 11425
tuned;
paulson [Fri, 13 Jul 2001 18:28:46 +0200] rev 11424
working
paulson [Fri, 13 Jul 2001 18:22:13 +0200] rev 11423
oops
paulson [Fri, 13 Jul 2001 18:20:26 +0200] rev 11422
fixed bad error in tdxbold; also removed default indexing in \\rulename
paulson [Fri, 13 Jul 2001 18:19:29 +0200] rev 11421
tweaks
paulson [Fri, 13 Jul 2001 18:08:26 +0200] rev 11420
added\\protect
paulson [Fri, 13 Jul 2001 18:07:01 +0200] rev 11419
more indexing
paulson [Fri, 13 Jul 2001 17:58:39 +0200] rev 11418
indexing tweaks
paulson [Fri, 13 Jul 2001 17:56:05 +0200] rev 11417
less indexing of theorem names
paulson [Fri, 13 Jul 2001 17:55:35 +0200] rev 11416
indexing
paulson [Fri, 13 Jul 2001 13:58:41 +0200] rev 11415
contrapos_pn
paulson [Fri, 13 Jul 2001 11:31:05 +0200] rev 11414
index file
paulson [Thu, 12 Jul 2001 17:36:14 +0200] rev 11413
removed a4paper
paulson [Thu, 12 Jul 2001 16:36:26 +0200] rev 11412
more in the Springer style
paulson [Thu, 12 Jul 2001 16:33:36 +0200] rev 11411
indexing
paulson [Wed, 11 Jul 2001 17:55:46 +0200] rev 11410
indexing
paulson [Wed, 11 Jul 2001 15:21:07 +0200] rev 11409
messages, and proper treatment of footnotes
paulson [Wed, 11 Jul 2001 15:10:07 +0200] rev 11408
new preface
paulson [Wed, 11 Jul 2001 14:00:48 +0200] rev 11407
tweaks for new version
paulson [Wed, 11 Jul 2001 13:57:01 +0200] rev 11406
indexing and tweaks
paulson [Wed, 11 Jul 2001 13:56:15 +0200] rev 11405
tweak
paulson [Wed, 11 Jul 2001 13:55:43 +0200] rev 11404
careful changes to make its output identical to that of indexing macros
paulson [Wed, 11 Jul 2001 13:55:15 +0200] rev 11403
new macro file for the tutorial
paulson [Wed, 11 Jul 2001 13:54:44 +0200] rev 11402
separate preface and macro file
paulson [Wed, 11 Jul 2001 10:50:18 +0200] rev 11401
do not remove Rules and Sets TeX files
paulson [Mon, 09 Jul 2001 13:43:02 +0200] rev 11400
isa-index replaces ../sedindex: knows about \\isa
paulson [Fri, 06 Jul 2001 16:04:32 +0200] rev 11399
two Isar tactic scripts
wenzelm [Tue, 03 Jul 2001 22:11:09 +0200] rev 11398
Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
uses of this ML file (HOL/Library is in the default load path);
paulson [Tue, 03 Jul 2001 15:40:25 +0200] rev 11397
GroupTheory
paulson [Tue, 03 Jul 2001 15:29:29 +0200] rev 11396
new lemmas
paulson [Tue, 03 Jul 2001 15:29:17 +0200] rev 11395
better treatment of restrict (lam)
paulson [Tue, 03 Jul 2001 15:28:24 +0200] rev 11394
Locale-based group theory proofs
wenzelm [Mon, 02 Jul 2001 21:53:11 +0200] rev 11393
ppc-darwin;
wenzelm [Mon, 02 Jul 2001 21:14:53 +0200] rev 11392
do *not* ./configure;
wenzelm [Mon, 02 Jul 2001 21:02:16 +0200] rev 11391
#!/usr/bin/env bash;
wenzelm [Mon, 02 Jul 2001 20:55:43 +0200] rev 11390
...
paulson [Fri, 29 Jun 2001 18:12:18 +0200] rev 11389
the records section
paulson [Fri, 29 Jun 2001 18:03:07 +0200] rev 11388
the records section
paulson [Fri, 29 Jun 2001 16:59:10 +0200] rev 11387
for the records section
paulson [Tue, 26 Jun 2001 17:25:41 +0200] rev 11386
a few new and/or improved results
paulson [Tue, 26 Jun 2001 17:07:02 +0200] rev 11385
gave Greatest_le its proper name
paulson [Tue, 26 Jun 2001 17:06:18 +0200] rev 11384
resolved name clash
paulson [Tue, 26 Jun 2001 17:05:10 +0200] rev 11383
tidied
paulson [Tue, 26 Jun 2001 17:04:54 +0200] rev 11382
now more like the HOL versions, and with the Square Root example added
paulson [Tue, 26 Jun 2001 17:04:09 +0200] rev 11381
tidying and consolidating files
paulson [Tue, 26 Jun 2001 16:54:39 +0200] rev 11380
tidying and consolidating files
nipkow [Tue, 26 Jun 2001 15:28:49 +0200] rev 11379
removed duplicate proof and small mod.
paulson [Mon, 25 Jun 2001 15:36:55 +0200] rev 11378
Simprocs for type "nat" no longer introduce numerals unless
paulson [Mon, 25 Jun 2001 15:35:59 +0200] rev 11377
Simprocs for type "nat" no longer introduce numerals unless they are already
present in the expression, and in a coefficient position (i.e. as a factor
of a monomial).
oheimb [Sat, 16 Jun 2001 20:06:42 +0200] rev 11376
added NanoJava
paulson [Wed, 13 Jun 2001 16:30:12 +0200] rev 11375
tidied
paulson [Wed, 13 Jun 2001 16:29:51 +0200] rev 11374
New proof of gcd_zero after a change to Divides.ML made the old one fail
paulson [Wed, 13 Jun 2001 16:28:40 +0200] rev 11373
a couple of new theorems
oheimb [Tue, 12 Jun 2001 14:11:00 +0200] rev 11372
corrected xsymbol/HTML syntax
berghofe [Mon, 11 Jun 2001 19:21:13 +0200] rev 11371
Fixed bug in function rebuild.
paulson [Sun, 10 Jun 2001 08:03:35 +0200] rev 11370
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
wenzelm [Sat, 09 Jun 2001 14:22:08 +0200] rev 11369
tuned
wenzelm [Sat, 09 Jun 2001 14:18:19 +0200] rev 11368
tuned Primes theory;
paulson [Sat, 09 Jun 2001 08:44:04 +0200] rev 11367
addition of the GREATEST quantifier
paulson [Sat, 09 Jun 2001 08:43:38 +0200] rev 11366
renaming of evs in the Fake rule
paulson [Sat, 09 Jun 2001 08:42:29 +0200] rev 11365
new material from the Sylow proof
paulson [Sat, 09 Jun 2001 08:42:06 +0200] rev 11364
simplified a proof using new dvd rules
paulson [Sat, 09 Jun 2001 08:41:25 +0200] rev 11363
moved Primes.thy from NumberTheory to Library
nipkow [Fri, 08 Jun 2001 08:50:08 +0200] rev 11362
Removed BCV
nipkow [Tue, 05 Jun 2001 09:51:04 +0200] rev 11361
*** empty log message ***
nipkow [Tue, 05 Jun 2001 09:41:11 +0200] rev 11360
This is now superseded by MicroJava/BV
paulson [Fri, 01 Jun 2001 11:04:19 +0200] rev 11359
renamed # to ## to avoid clashing with List cons
paulson [Fri, 01 Jun 2001 11:03:50 +0200] rev 11358
now checks for leading meta-quantifiers and complains, instead of
just raising an exception
wenzelm [Thu, 31 May 2001 22:34:58 +0200] rev 11357
tuned
wenzelm [Thu, 31 May 2001 20:53:49 +0200] rev 11356
added HOL-CTL;
wenzelm [Thu, 31 May 2001 20:52:51 +0200] rev 11355
tuned
paulson [Thu, 31 May 2001 18:28:23 +0200] rev 11354
examples files start from Main instead of various ZF theories
wenzelm [Thu, 31 May 2001 17:57:02 +0200] rev 11353
invent_names
bauerg [Thu, 31 May 2001 17:24:56 +0200] rev 11352
added HOL-CTL example;
oheimb [Thu, 31 May 2001 17:06:00 +0200] rev 11351
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb [Thu, 31 May 2001 16:53:00 +0200] rev 11350
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb [Thu, 31 May 2001 16:52:54 +0200] rev 11349
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb [Thu, 31 May 2001 16:52:47 +0200] rev 11348
added stream length, map, and filter
oheimb [Thu, 31 May 2001 16:52:35 +0200] rev 11347
corrected ML names of definitions, added chain_shift
oheimb [Thu, 31 May 2001 16:52:32 +0200] rev 11346
corrected ML names of definitions
oheimb [Thu, 31 May 2001 16:52:20 +0200] rev 11345
improved iff_add_global, new function add_rules factoring out common behaviour
oheimb [Thu, 31 May 2001 16:52:02 +0200] rev 11344
streamlined addIffs/delIffs, added warnings
oheimb [Thu, 31 May 2001 16:51:26 +0200] rev 11343
replaced Sel_injective_cprod by new injective_fst_snd
oheimb [Thu, 31 May 2001 16:51:14 +0200] rev 11342
added lub_range_mono and lub_range_shift
oheimb [Thu, 31 May 2001 16:50:17 +0200] rev 11341
added chain_monofun
oheimb [Thu, 31 May 2001 16:50:16 +0200] rev 11340
added same_fstI as safe intro rule
oheimb [Thu, 31 May 2001 16:50:15 +0200] rev 11339
added injective_fst_snd
oheimb [Thu, 31 May 2001 16:50:14 +0200] rev 11338
added nat_not_singleton (also to simpset)
oheimb [Thu, 31 May 2001 16:50:13 +0200] rev 11337
added Least_Suc2
oheimb [Thu, 31 May 2001 16:50:04 +0200] rev 11336
added list_all2_trans
oheimb [Thu, 31 May 2001 16:17:28 +0200] rev 11335
added weak_coinduct_image
nipkow [Thu, 31 May 2001 16:07:35 +0200] rev 11334
Allow Suc-numerals as coefficients in lin-arith formulae
oheimb [Thu, 31 May 2001 12:43:56 +0200] rev 11333
corrected entry for iff attribute
oheimb [Wed, 30 May 2001 18:54:10 +0200] rev 11332
extended doc for iff attribute
bauerg [Wed, 30 May 2001 10:48:59 +0200] rev 11331
injectivity of ^;
paulson [Tue, 29 May 2001 11:43:12 +0200] rev 11330
deleted a needless reference to rtrancl_unfold
oheimb [Mon, 28 May 2001 18:48:28 +0200] rev 11329
improved handling of space before/after parentheses
berghofe [Tue, 22 May 2001 15:15:16 +0200] rev 11328
Inductive characterization of wfrec combinator.
berghofe [Tue, 22 May 2001 15:12:11 +0200] rev 11327
Transitive closure is now defined via "inductive".
berghofe [Tue, 22 May 2001 15:11:43 +0200] rev 11326
Representing set for type nat is now defined via "inductive".
berghofe [Tue, 22 May 2001 15:10:06 +0200] rev 11325
Inductive definitions are now introduced earlier in the theory hierarchy.
paulson [Tue, 22 May 2001 09:26:57 +0200] rev 11324
nat_diff_split_asm, for the assumptions
paulson [Mon, 21 May 2001 14:53:30 +0200] rev 11323
if_splits and split_if_asm
paulson [Mon, 21 May 2001 14:53:11 +0200] rev 11322
fixed the X-symbol syntax for lambda
paulson [Mon, 21 May 2001 14:52:27 +0200] rev 11321
the rest of integer division
paulson [Mon, 21 May 2001 14:52:04 +0200] rev 11320
X-symbols for set theory
paulson [Mon, 21 May 2001 14:51:46 +0200] rev 11319
X-symbols for ZF
paulson [Mon, 21 May 2001 14:46:30 +0200] rev 11318
X-symbols for ZF
paulson [Mon, 21 May 2001 14:45:52 +0200] rev 11317
X-symbols for set theory
paulson [Mon, 21 May 2001 14:36:24 +0200] rev 11316
X-symbols for set theory
paulson [Mon, 21 May 2001 14:35:54 +0200] rev 11315
Division examples
paulson [Mon, 21 May 2001 12:51:15 +0200] rev 11314
ZF: division
paulson [Sun, 20 May 2001 13:16:27 +0200] rev 11313
new theorem dvd_mult_right
nipkow [Sun, 20 May 2001 11:20:41 +0200] rev 11312
added (no)_type_brackets
paulson [Sat, 19 May 2001 12:21:34 +0200] rev 11311
power_le_dvd replaces power_less_dvd
paulson [Sat, 19 May 2001 12:19:23 +0200] rev 11310
spelling check
paulson [Fri, 18 May 2001 17:18:43 +0200] rev 11309
minor suggestions by Tanja Vos
nipkow [Fri, 18 May 2001 16:45:55 +0200] rev 11308
*** empty log message ***
nipkow [Fri, 18 May 2001 12:13:53 +0200] rev 11307
*** empty log message ***
nipkow [Fri, 18 May 2001 12:09:13 +0200] rev 11306
added comments
nipkow [Fri, 18 May 2001 07:56:19 +0200] rev 11305
added ^ on functions.
paulson [Thu, 17 May 2001 11:31:21 +0200] rev 11304
auto update
paulson [Thu, 17 May 2001 11:31:08 +0200] rev 11303
typo, etc.
paulson [Thu, 17 May 2001 11:29:04 +0200] rev 11302
minor revisons
paulson [Wed, 16 May 2001 18:03:12 +0200] rev 11301
spelling
paulson [Wed, 16 May 2001 17:58:48 +0200] rev 11300
typo
nipkow [Wed, 16 May 2001 12:31:25 +0200] rev 11299
welltyping -> wt_step
nipkow [Mon, 14 May 2001 09:58:22 +0200] rev 11298
simplified defs and proofs a little
nipkow [Fri, 11 May 2001 15:57:42 +0200] rev 11297
mult_Suc generally, not just for numerals.
nipkow [Fri, 11 May 2001 13:49:15 +0200] rev 11296
added mult_Suc laws to lin.arith.simpset.
removed Suc n = n + #1 added earlier - #1::nat is not expected by Larry's
simprocs.
nipkow [Thu, 10 May 2001 17:28:40 +0200] rev 11295
improved tracing of permutative rules.
nipkow [Thu, 10 May 2001 13:44:44 +0200] rev 11294
*** empty log message ***
nipkow [Thu, 10 May 2001 09:48:50 +0200] rev 11293
*** empty log message ***
nipkow [Thu, 10 May 2001 09:41:45 +0200] rev 11292
*** empty log message ***
nipkow [Wed, 09 May 2001 23:09:26 +0200] rev 11291
improved simproc trace IGNORED
paulson [Tue, 08 May 2001 16:01:36 +0200] rev 11290
fixed comment
paulson [Tue, 08 May 2001 16:01:28 +0200] rev 11289
new takeWhile lemma
paulson [Tue, 08 May 2001 15:57:13 +0200] rev 11288
fixed a slow proof; tidied
paulson [Tue, 08 May 2001 15:56:57 +0200] rev 11287
conversion of Auth/TLS to Isar script
oheimb [Mon, 07 May 2001 19:19:41 +0200] rev 11286
minor bugfix for AddIffs
nipkow [Fri, 04 May 2001 15:39:38 +0200] rev 11285
*** empty log message ***
nipkow [Fri, 04 May 2001 15:38:48 +0200] rev 11284
made same_fst recdef_simp
oheimb [Thu, 03 May 2001 18:22:36 +0200] rev 11283
improved EVERY'
nipkow [Thu, 03 May 2001 17:51:29 +0200] rev 11282
*** empty log message ***
paulson [Thu, 03 May 2001 11:53:42 +0200] rev 11281
minor tweaks
paulson [Thu, 03 May 2001 10:27:37 +0200] rev 11280
minor tweaks
paulson [Thu, 03 May 2001 10:27:04 +0200] rev 11279
remove unnecessary TeX files
nipkow [Wed, 02 May 2001 11:54:18 +0200] rev 11278
*** empty log message ***
nipkow [Tue, 01 May 2001 22:26:55 +0200] rev 11277
*** empty log message ***
paulson [Tue, 01 May 2001 17:16:32 +0200] rev 11276
to ignore the *.class files that are copied here
nipkow [Mon, 30 Apr 2001 19:26:04 +0200] rev 11275
new proof
oheimb [Mon, 30 Apr 2001 13:54:33 +0200] rev 11274
minor bugfix for subst_RS
oheimb [Mon, 30 Apr 2001 13:17:17 +0200] rev 11273
improve support for EVERY', added support for EVERY
oheimb [Mon, 30 Apr 2001 12:15:25 +0200] rev 11272
minor bugfix for newlines with Goalw
oheimb [Mon, 30 Apr 2001 11:57:10 +0200] rev 11271
added support for EVERY', improved support for RS
paulson [Fri, 27 Apr 2001 17:16:21 +0200] rev 11270
better treatment of methods: uses Method.ctxt_args to refer to current
simpset and claset. Needed to fix problems with Recur.thy
paulson [Wed, 25 Apr 2001 10:31:39 +0200] rev 11269
changes specifically for the book version
paulson [Tue, 24 Apr 2001 17:55:06 +0200] rev 11268
new reference: Yahalom
paulson [Tue, 24 Apr 2001 17:54:49 +0200] rev 11267
revisions to Protocols chapter
oheimb [Tue, 24 Apr 2001 14:26:05 +0200] rev 11266
simplified proofs concerning class_rec
paulson [Tue, 24 Apr 2001 12:19:58 +0200] rev 11265
removal of image_Collect as a default simprule
paulson [Tue, 24 Apr 2001 12:19:01 +0200] rev 11264
(rough) conversion of Auth/Recur to Isar format
oheimb [Mon, 23 Apr 2001 17:11:19 +0200] rev 11263
added parentheses for 'b y' syntax, added primitive smp_tac support
nipkow [Fri, 20 Apr 2001 17:18:47 +0200] rev 11262
*** empty log message ***
paulson [Fri, 20 Apr 2001 11:11:40 +0200] rev 11261
suggestions from OHeimb
paulson [Thu, 19 Apr 2001 15:42:53 +0200] rev 11260
renaming of theory LOmega to lomega2 in order to prevent a possible
case confusion
nipkow [Thu, 19 Apr 2001 13:36:07 +0200] rev 11259
*** empty log message ***
wenzelm [Wed, 18 Apr 2001 22:09:45 +0200] rev 11258
polyml-4.1;
nipkow [Tue, 17 Apr 2001 19:28:04 +0200] rev 11257
*** empty log message ***
nipkow [Tue, 17 Apr 2001 16:54:38 +0200] rev 11256
*** empty log message ***
paulson [Tue, 17 Apr 2001 15:03:41 +0200] rev 11255
*** empty log message ***
wenzelm [Mon, 16 Apr 2001 15:34:33 +0200] rev 11254
TODO
wenzelm [Thu, 12 Apr 2001 18:05:41 +0200] rev 11253
proper order of order_less_asym';
kleing [Thu, 12 Apr 2001 13:40:15 +0200] rev 11252
cleanup, tuned
paulson [Thu, 12 Apr 2001 12:45:05 +0200] rev 11251
converted many HOL/Auth theories to Isar scripts
paulson [Wed, 11 Apr 2001 11:53:54 +0200] rev 11250
symlinks to ../../../HOL/Auth. Fingers crossed...
paulson [Tue, 10 Apr 2001 16:11:01 +0200] rev 11249
Protocols chapter
paulson [Tue, 10 Apr 2001 16:09:26 +0200] rev 11248
back to Unix format...
paulson [Tue, 10 Apr 2001 16:02:01 +0200] rev 11247
security protocol chapter
paulson [Tue, 10 Apr 2001 15:58:50 +0200] rev 11246
security protocol refs
paulson [Mon, 09 Apr 2001 14:49:51 +0200] rev 11245
new theorem Fake_parts_insert_in_Un
paulson [Mon, 09 Apr 2001 10:12:33 +0200] rev 11244
extra display
paulson [Mon, 09 Apr 2001 10:12:12 +0200] rev 11243
*** empty log message ***
paulson [Mon, 09 Apr 2001 10:11:59 +0200] rev 11242
lexicographic product of two relations: updated HOL.tex
Also automatic updates by xemacs
paulson [Mon, 09 Apr 2001 10:10:21 +0200] rev 11241
Isar hint
wenzelm [Sat, 07 Apr 2001 19:38:50 +0200] rev 11240
thm output: Attrib.local_thmss;
wenzelm [Sat, 07 Apr 2001 19:38:01 +0200] rev 11239
tuned
nipkow [Fri, 30 Mar 2001 18:35:33 +0200] rev 11238
*** empty log message ***
nipkow [Fri, 30 Mar 2001 18:18:22 +0200] rev 11237
*** empty log message ***
nipkow [Fri, 30 Mar 2001 18:12:26 +0200] rev 11236
*** empty log message ***
nipkow [Fri, 30 Mar 2001 16:12:57 +0200] rev 11235
*** empty log message ***
paulson [Fri, 30 Mar 2001 13:29:16 +0200] rev 11234
quantifier instantiation
paulson [Fri, 30 Mar 2001 12:31:10 +0200] rev 11233
the one-point rule for bounded quantifiers
nipkow [Thu, 29 Mar 2001 13:59:54 +0200] rev 11232
generalization of 1 point rules for ALL
nipkow [Thu, 29 Mar 2001 12:26:37 +0200] rev 11231
*** empty log message ***
paulson [Thu, 29 Mar 2001 10:44:37 +0200] rev 11230
misc tidying; changing the predicate isSymKey to the set symKeys
nipkow [Wed, 28 Mar 2001 13:40:06 +0200] rev 11229
Got rid of is_dfa
nipkow [Wed, 28 Mar 2001 13:39:50 +0200] rev 11228
MicroJava/BV dependencies incomplete
nipkow [Tue, 27 Mar 2001 13:00:30 +0200] rev 11227
fixed bug in tactic for ball 1 point simproc
paulson [Tue, 27 Mar 2001 11:27:06 +0200] rev 11226
Vos
nipkow [Mon, 26 Mar 2001 19:37:31 +0200] rev 11225
simplified proofs
nipkow [Mon, 26 Mar 2001 16:31:38 +0200] rev 11224
simplified proofs
nipkow [Mon, 26 Mar 2001 12:51:14 +0200] rev 11223
I forgot a few bases cases for the 1-point rules...
paulson [Fri, 23 Mar 2001 12:10:05 +0100] rev 11222
shortening and streamlining of proofs
nipkow [Fri, 23 Mar 2001 10:12:12 +0100] rev 11221
added simproc for bounded quantifiers
nipkow [Fri, 23 Mar 2001 10:10:53 +0100] rev 11220
added one point simprocs for bounded quantifiers
paulson [Thu, 22 Mar 2001 10:29:26 +0100] rev 11219
new theorem analz_Decrypt'
paulson [Thu, 22 Mar 2001 10:28:46 +0100] rev 11218
new theorem analz_isSymKey_Decrypt
paulson [Thu, 22 Mar 2001 10:27:00 +0100] rev 11217
some X-symbols
nipkow [Mon, 19 Mar 2001 17:25:42 +0100] rev 11216
*** empty log message ***
nipkow [Mon, 19 Mar 2001 13:28:06 +0100] rev 11215
*** empty log message ***
nipkow [Mon, 19 Mar 2001 13:05:56 +0100] rev 11214
*** empty log message ***
nipkow [Mon, 19 Mar 2001 12:38:36 +0100] rev 11213
*** empty log message ***
paulson [Mon, 19 Mar 2001 10:37:47 +0100] rev 11212
*** empty log message ***
paulson [Thu, 15 Mar 2001 16:56:35 +0100] rev 11211
translations: a tweak
nipkow [Thu, 15 Mar 2001 15:05:51 +0100] rev 11210
*** empty log message ***
nipkow [Thu, 15 Mar 2001 13:57:10 +0100] rev 11209
*** empty log message ***
nipkow [Thu, 15 Mar 2001 11:06:33 +0100] rev 11208
*** empty log message ***
nipkow [Thu, 15 Mar 2001 10:41:32 +0100] rev 11207
*** empty log message ***
nipkow [Wed, 14 Mar 2001 18:40:01 +0100] rev 11206
*** empty log message ***
nipkow [Wed, 14 Mar 2001 17:38:49 +0100] rev 11205
*** empty log message ***
paulson [Wed, 14 Mar 2001 08:50:55 +0100] rev 11204
minor tuning
nipkow [Tue, 13 Mar 2001 18:35:48 +0100] rev 11203
*** empty log message ***
nipkow [Mon, 12 Mar 2001 18:23:11 +0100] rev 11202
*** empty log message ***
nipkow [Mon, 12 Mar 2001 18:17:45 +0100] rev 11201
*** empty log message ***
nipkow [Fri, 09 Mar 2001 19:05:48 +0100] rev 11200
arith_tac now copes with propositional reasoning as well.
paulson [Wed, 07 Mar 2001 18:35:27 +0100] rev 11199
expanded abbrevs
streckem [Wed, 07 Mar 2001 17:19:16 +0100] rev 11198
added strange 'b y' syntax
nipkow [Wed, 07 Mar 2001 16:25:51 +0100] rev 11197
*** empty log message ***
nipkow [Wed, 07 Mar 2001 15:54:11 +0100] rev 11196
*** empty log message ***
paulson [Mon, 05 Mar 2001 15:47:11 +0100] rev 11195
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson [Mon, 05 Mar 2001 15:32:54 +0100] rev 11194
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson [Mon, 05 Mar 2001 15:25:11 +0100] rev 11193
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson [Mon, 05 Mar 2001 12:31:31 +0100] rev 11192
a few basic X-symbols
paulson [Fri, 02 Mar 2001 13:26:55 +0100] rev 11191
conversion of Message.thy to Isar format
ehmety [Fri, 02 Mar 2001 13:18:56 +0100] rev 11190
*** empty log message ***
paulson [Fri, 02 Mar 2001 13:18:31 +0100] rev 11189
conversion of Message.thy to Isar format
paulson [Fri, 02 Mar 2001 13:14:37 +0100] rev 11188
streamlined a proof
paulson [Wed, 28 Feb 2001 12:37:48 +0100] rev 11187
auto-update
nipkow [Tue, 27 Feb 2001 23:25:47 +0100] rev 11186
*** empty log message ***
paulson [Tue, 27 Feb 2001 16:13:23 +0100] rev 11185
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Streamlining of Yahalom proofs
Removal of redundant proofs
nipkow [Tue, 27 Feb 2001 12:28:42 +0100] rev 11184
kildall now via while and therefore executable!
paulson [Mon, 26 Feb 2001 16:36:53 +0100] rev 11183
minor tweaks to speed the proofs
paulson [Mon, 26 Feb 2001 10:41:24 +0100] rev 11182
minor fixes
oheimb [Fri, 23 Feb 2001 16:31:21 +0100] rev 11181
renamed addaltern to addafter, addSaltern to addSafter
oheimb [Fri, 23 Feb 2001 16:31:18 +0100] rev 11180
removed performance leak for split_conv_tac (and corresponding safe wrapper)
paulson [Thu, 22 Feb 2001 18:13:23 +0100] rev 11179
subst method and a new section on rule, rule_tac, etc
kleing [Thu, 22 Feb 2001 18:03:11 +0100] rev 11178
removed unused constant
kleing [Thu, 22 Feb 2001 11:47:35 +0100] rev 11177
removed unused function
paulson [Thu, 22 Feb 2001 11:31:31 +0100] rev 11176
a PROPER tidy-up
nipkow [Thu, 22 Feb 2001 10:18:41 +0100] rev 11175
recoded function iter with the help of the while-combinator.
paulson [Wed, 21 Feb 2001 15:21:15 +0100] rev 11174
revisions in response to comments by Tobias
paulson [Wed, 21 Feb 2001 12:57:55 +0100] rev 11173
revisions in response to comments by Tobias
oheimb [Wed, 21 Feb 2001 12:07:00 +0100] rev 11172
added split_conv_tac (also to claset()) as an optimization
oheimb [Tue, 20 Feb 2001 18:53:28 +0100] rev 11171
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
oheimb [Tue, 20 Feb 2001 18:48:34 +0100] rev 11170
simplified proofs for splitI and splitD, added splitD'
added split_conv_tac (also to claset()) as an optimization
made split_all_tac safe introducing safe_full_simp_tac,EXISTING PROOFS MAY FAIL
oheimb [Tue, 20 Feb 2001 18:47:34 +0100] rev 11169
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
oheimb [Tue, 20 Feb 2001 18:47:32 +0100] rev 11168
corrected comments on addbefore and addSbefore
oheimb [Tue, 20 Feb 2001 18:47:30 +0100] rev 11167
added same_fstI
oheimb [Tue, 20 Feb 2001 18:47:29 +0100] rev 11166
simplified definition of wrapper bspec
oheimb [Tue, 20 Feb 2001 18:47:27 +0100] rev 11165
added image_cong to default congs of recdef
oheimb [Tue, 20 Feb 2001 18:47:25 +0100] rev 11164
added add_arith (just as hint by now)
oheimb [Tue, 20 Feb 2001 18:47:22 +0100] rev 11163
added rearrange_prems
oheimb [Tue, 20 Feb 2001 18:47:06 +0100] rev 11162
debugging: replaced gen_all by forall_elim_vars_safe
nipkow [Tue, 20 Feb 2001 13:23:58 +0100] rev 11161
*** empty log message ***
nipkow [Tue, 20 Feb 2001 11:27:04 +0100] rev 11160
*** empty log message ***
nipkow [Tue, 20 Feb 2001 10:37:12 +0100] rev 11159
*** empty log message ***
nipkow [Tue, 20 Feb 2001 10:18:26 +0100] rev 11158
*** empty log message ***
nipkow [Sat, 17 Feb 2001 10:43:53 +0100] rev 11157
*** empty log message ***
paulson [Fri, 16 Feb 2001 18:51:19 +0100] rev 11156
fixed the obvious errors Tobias found
paulson [Fri, 16 Feb 2001 18:50:09 +0100] rev 11155
Least_def now refers to LeastM
paulson [Fri, 16 Feb 2001 13:47:06 +0100] rev 11154
for the change to LEAST
paulson [Fri, 16 Feb 2001 13:37:21 +0100] rev 11153
Blast bug fix made old proof too slow
paulson [Fri, 16 Feb 2001 13:29:07 +0100] rev 11152
Blast bug fix: now always duplicates when applying a haz rule,
whether or not new variables are added.
Can now prove theorems such as these:
val prems = Goal "[|P==>Q; P==>~Q|] ==> ~P";
by (blast_tac (claset() addDs prems) 1);
val prems = Goal "[|Q==>P; ~Q==>P|] ==> P";
by (blast_tac (claset() addIs prems) 1);
paulson [Fri, 16 Feb 2001 13:27:56 +0100] rev 11151
Blast bug fix made old proof too slow
paulson [Fri, 16 Feb 2001 13:25:08 +0100] rev 11150
Streamlining for the bug fix in Blast.
MPair_parts now built in using AddSEs, throughout.
nipkow [Fri, 16 Feb 2001 08:27:17 +0100] rev 11149
*** empty log message ***
nipkow [Fri, 16 Feb 2001 08:10:28 +0100] rev 11148
*** empty log message ***
nipkow [Fri, 16 Feb 2001 06:46:20 +0100] rev 11147
*** empty log message ***
wenzelm [Fri, 16 Feb 2001 00:36:21 +0100] rev 11146
tuned;
wenzelm [Thu, 15 Feb 2001 17:18:54 +0100] rev 11145
eliminate get_def;
wenzelm [Thu, 15 Feb 2001 16:12:27 +0100] rev 11144
tuned;
oheimb [Thu, 15 Feb 2001 16:07:57 +0100] rev 11143
Ord.thy/.ML converted to Isar
oheimb [Thu, 15 Feb 2001 16:01:47 +0100] rev 11142
moved inv_image to Relation
nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML
added wf_linord_ex_has_least,LeastM_nat_lemma,LeastM_natI,LeastM_nat_le
oheimb [Thu, 15 Feb 2001 16:01:34 +0100] rev 11141
supressed some warnings on identical proofstate
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
from Nat.ML to Wellfounded_Recursion.ML
added wellorder axclass
oheimb [Thu, 15 Feb 2001 16:01:22 +0100] rev 11140
Ord.thy/.ML converted to Isar
added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy
moved Least_equality from Nat.ML to Ord.thy
added LeastM operator
oheimb [Thu, 15 Feb 2001 16:01:07 +0100] rev 11139
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
from Nat.ML to Wellfounded_Recursion.ML
moved Least_equality from Nat.ML to Ord.thy
moved wf_less from Nat.ML to NatDef.ML
added wellorder axclass
nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML
added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy
oheimb [Thu, 15 Feb 2001 16:00:44 +0100] rev 11138
simplified proof of Least_mono
oheimb [Thu, 15 Feb 2001 16:00:42 +0100] rev 11137
added wellorder axclass
oheimb [Thu, 15 Feb 2001 16:00:40 +0100] rev 11136
moved inv_image to Relation
oheimb [Thu, 15 Feb 2001 16:00:38 +0100] rev 11135
moved wf_less from Nat.ML to NatDef.ML
oheimb [Thu, 15 Feb 2001 16:00:36 +0100] rev 11134
added nat as instance of new wellorder axclass
oheimb [Thu, 15 Feb 2001 16:00:35 +0100] rev 11133
Ord.thy/.ML converted to Isar
oheimb [Thu, 15 Feb 2001 15:56:51 +0100] rev 11132
added trial proof
oheimb [Thu, 15 Feb 2001 14:30:13 +0100] rev 11131
improved subst_RS
oheimb [Thu, 15 Feb 2001 13:07:03 +0100] rev 11130
added missiong word
nipkow [Thu, 15 Feb 2001 11:15:39 +0100] rev 11129
*** empty log message ***
wenzelm [Thu, 15 Feb 2001 00:53:45 +0100] rev 11128
index mod syntax;
wenzelm [Wed, 14 Feb 2001 23:43:55 +0100] rev 11127
tuned;
wenzelm [Wed, 14 Feb 2001 23:42:45 +0100] rev 11126
isatool install -k;
wenzelm [Wed, 14 Feb 2001 23:18:47 +0100] rev 11125
handle KDE version 1 or 2;
wenzelm [Wed, 14 Feb 2001 23:17:53 +0100] rev 11124
isatool install handles KDE version 1 or 2;
oheimb [Wed, 14 Feb 2001 20:45:35 +0100] rev 11123
removed whitespace
oheimb [Wed, 14 Feb 2001 20:44:59 +0100] rev 11122
supressed some warnings on identical proofstate
wenzelm [Wed, 14 Feb 2001 19:31:05 +0100] rev 11121
adhoc script for creating complete Isabelle dist pages;
berghofe [Wed, 14 Feb 2001 19:27:49 +0100] rev 11120
imp_cong2 -> imp_cong
paulson [Wed, 14 Feb 2001 13:26:46 +0100] rev 11119
new function get_overloads
paulson [Wed, 14 Feb 2001 13:19:14 +0100] rev 11118
updated the unicity proof
paulson [Wed, 14 Feb 2001 13:01:02 +0100] rev 11117
tidying
paulson [Wed, 14 Feb 2001 12:22:49 +0100] rev 11116
not_bad_tac is obsolete
paulson [Wed, 14 Feb 2001 12:16:32 +0100] rev 11115
a new theorem from Bryan Ford
oheimb [Wed, 14 Feb 2001 11:18:39 +0100] rev 11114
added support for AddXIs, AddXEs, AddXDs
wenzelm [Wed, 14 Feb 2001 01:36:36 +0100] rev 11113
tuned;
wenzelm [Tue, 13 Feb 2001 22:51:08 +0100] rev 11112
tuned;
wenzelm [Tue, 13 Feb 2001 22:04:09 +0100] rev 11111
tuned;
wenzelm [Tue, 13 Feb 2001 16:48:36 +0100] rev 11110
\remarksfalse;
wenzelm [Tue, 13 Feb 2001 16:31:18 +0100] rev 11109
tuned;
paulson [Tue, 13 Feb 2001 16:05:56 +0100] rev 11108
swapped Fleuriot and Paulson
wenzelm [Tue, 13 Feb 2001 16:05:09 +0100] rev 11107
create dist packages;
paulson [Tue, 13 Feb 2001 16:02:53 +0100] rev 11106
partial conversion to Isar script style in HOL/Auth removes some .ML files
paulson [Tue, 13 Feb 2001 15:46:03 +0100] rev 11105
partial conversion to Isar script style in HOL/Auth removes some .ML files
paulson [Tue, 13 Feb 2001 13:16:27 +0100] rev 11104
partial conversion to Isar script style
simplified unicity proofs
wenzelm [Tue, 13 Feb 2001 01:32:54 +0100] rev 11103
tuned;
wenzelm [Mon, 12 Feb 2001 20:47:19 +0100] rev 11102
tuned;
wenzelm [Mon, 12 Feb 2001 20:45:12 +0100] rev 11101
support \<subseteq> syntax in classes/classrel/axclass/instance;
wenzelm [Mon, 12 Feb 2001 20:44:02 +0100] rev 11100
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm [Mon, 12 Feb 2001 20:43:12 +0100] rev 11099
\<subseteq>;
wenzelm [Sun, 11 Feb 2001 20:38:40 +0100] rev 11098
added "xsymbols" syntax for "=?=";
wenzelm [Sun, 11 Feb 2001 16:34:20 +0100] rev 11097
more robust selection of calculational rules;
wenzelm [Sun, 11 Feb 2001 16:31:54 +0100] rev 11096
tuned trans rules;
wenzelm [Sun, 11 Feb 2001 16:31:21 +0100] rev 11095
updated;
wenzelm [Sun, 11 Feb 2001 13:26:23 +0100] rev 11094
tuned;
ballarin [Sat, 10 Feb 2001 08:52:41 +0100] rev 11093
Changes to HOL/Algebra:
- Axclasses consolidated (axiom one_not_zero).
- Now uses summation operator setsum; SUM has been removed.
- Priority of infix assoc changed to 50, in accordance to dvd.
ballarin [Sat, 10 Feb 2001 08:49:36 +0100] rev 11092
Definition of setsum (sort constraint) relaxed to {zero, plus}.
ballarin [Sat, 10 Feb 2001 08:48:10 +0100] rev 11091
Updates to HOL/Algebra:
- axclasses consolidated (lemma one_not_zero)
- summation operator SUM removed, now uses setsum
Use of setsum made it necessary to relax sort constraint in its definition
to {zero, plus}.
wenzelm [Fri, 09 Feb 2001 23:48:50 +0100] rev 11090
tuned;
wenzelm [Fri, 09 Feb 2001 23:48:33 +0100] rev 11089
lower priority for forw_subst;
wenzelm [Fri, 09 Feb 2001 20:34:42 +0100] rev 11088
tuned;
kleing [Fri, 09 Feb 2001 16:23:40 +0100] rev 11087
not used any more (all Isar style)
kleing [Fri, 09 Feb 2001 16:22:30 +0100] rev 11086
removed MicroJava/Digest.thy
kleing [Fri, 09 Feb 2001 16:01:58 +0100] rev 11085
tuned for 99-2 release
wenzelm [Fri, 09 Feb 2001 11:40:10 +0100] rev 11084
unsymbolized;
tuned;
wenzelm [Wed, 07 Feb 2001 20:57:03 +0100] rev 11083
tuned;
wenzelm [Wed, 07 Feb 2001 20:56:40 +0100] rev 11082
improved;
oheimb [Wed, 07 Feb 2001 17:40:56 +0100] rev 11081
solved non-initialization problems; improvements using prefer
paulson [Wed, 07 Feb 2001 16:37:24 +0100] rev 11080
various revisions in response to comments from Tobias
wenzelm [Wed, 07 Feb 2001 12:15:59 +0100] rev 11079
val get_goal: state -> context * (thm list * thm);
wenzelm [Tue, 06 Feb 2001 18:41:27 +0100] rev 11078
4.0 version;
paulson [Tue, 06 Feb 2001 18:37:59 +0100] rev 11077
snapshot of a new version
paulson [Tue, 06 Feb 2001 15:02:56 +0100] rev 11076
new theorem Transset_iff_Union_subset
kleing [Tue, 06 Feb 2001 14:42:28 +0100] rev 11075
tuned
wenzelm [Mon, 05 Feb 2001 21:33:47 +0100] rev 11074
improved;
wenzelm [Mon, 05 Feb 2001 20:44:51 +0100] rev 11073
polyml multiplatform setup;
wenzelm [Mon, 05 Feb 2001 20:34:05 +0100] rev 11072
tuned
wenzelm [Mon, 05 Feb 2001 20:33:50 +0100] rev 11071
tuned;
oheimb [Mon, 05 Feb 2001 20:14:15 +0100] rev 11070
improved document (added headers etc)
wenzelm [Mon, 05 Feb 2001 14:59:44 +0100] rev 11069
tuned
oheimb [Mon, 05 Feb 2001 14:57:17 +0100] rev 11068
improvements concerning instantiations etc.
wenzelm [Mon, 05 Feb 2001 14:54:04 +0100] rev 11067
disable non-existant chapters
wenzelm [Mon, 05 Feb 2001 14:40:21 +0100] rev 11066
tuned;
wenzelm [Mon, 05 Feb 2001 14:39:09 +0100] rev 11065
fixed version string;
wenzelm [Mon, 05 Feb 2001 14:38:11 +0100] rev 11064
polyml-3.x.ML vs polyml-4.0.ML;
wenzelm [Mon, 05 Feb 2001 14:37:10 +0100] rev 11063
renamed polyml.ML to polyml-3.x.ML and polyml-4.0.ML to polyml.ML (default);
wenzelm [Mon, 05 Feb 2001 14:31:49 +0100] rev 11062
tuned;
wenzelm [Mon, 05 Feb 2001 14:30:55 +0100] rev 11061
example Proof General settings;
wenzelm [Sun, 04 Feb 2001 22:34:52 +0100] rev 11060
document setup;
wenzelm [Sun, 04 Feb 2001 22:28:31 +0100] rev 11059
converted to new-style;
wenzelm [Sun, 04 Feb 2001 19:46:31 +0100] rev 11058
moved theory Perm to HOL/Library;
wenzelm [Sun, 04 Feb 2001 19:44:09 +0100] rev 11057
added no_document
wenzelm [Sun, 04 Feb 2001 19:43:32 +0100] rev 11056
tuned
wenzelm [Sun, 04 Feb 2001 19:43:15 +0100] rev 11055
added Permutation;
wenzelm [Sun, 04 Feb 2001 19:42:54 +0100] rev 11054
moved from Induct/ to Library/
wenzelm [Sun, 04 Feb 2001 19:41:47 +0100] rev 11053
updated
wenzelm [Sun, 04 Feb 2001 19:41:30 +0100] rev 11052
added no_document;
wenzelm [Sun, 04 Feb 2001 19:40:54 +0100] rev 11051
updated split_format;
wenzelm [Sun, 04 Feb 2001 19:40:06 +0100] rev 11050
* no_document ML operator temporarily disables LaTeX document
generation;
wenzelm [Sun, 04 Feb 2001 19:31:13 +0100] rev 11049
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm [Sat, 03 Feb 2001 17:43:34 +0100] rev 11048
tuned msg;
wenzelm [Sat, 03 Feb 2001 17:43:05 +0100] rev 11047
tuned;
wenzelm [Sat, 03 Feb 2001 17:40:16 +0100] rev 11046
Induct: converted some theories to new-style format;
wenzelm [Sat, 03 Feb 2001 15:22:57 +0100] rev 11045
fixed syntax of 'split_format';
wenzelm [Sat, 03 Feb 2001 15:21:57 +0100] rev 11044
use fgrep;
wenzelm [Sat, 03 Feb 2001 15:20:55 +0100] rev 11043
HOL: inductive package no longer splits induction rule aggressively,
but only as far as specified by the introductions given; the old
format may recovered via ML function complete_split_rule or attribute
'split_rule (complete)';
paulson [Sat, 03 Feb 2001 12:41:38 +0100] rev 11042
commutation theory, ported by Sidi Ehmety
wenzelm [Sat, 03 Feb 2001 00:11:07 +0100] rev 11041
updated;
wenzelm [Sat, 03 Feb 2001 00:01:54 +0100] rev 11040
simplified 'split_format' syntax;
wenzelm [Fri, 02 Feb 2001 23:59:30 +0100] rev 11039
'split_format' attribute;
wenzelm [Fri, 02 Feb 2001 22:21:06 +0100] rev 11038
tuned;
wenzelm [Fri, 02 Feb 2001 22:20:43 +0100] rev 11037
module setup;
use hidden internal_split constants;
wenzelm [Fri, 02 Feb 2001 22:20:09 +0100] rev 11036
use hol_simplify;
wenzelm [Fri, 02 Feb 2001 22:19:52 +0100] rev 11035
use hol_rewrite_cterm;
wenzelm [Fri, 02 Feb 2001 22:19:23 +0100] rev 11034
added hol_simplify, hol_rewrite_cterm;
wenzelm [Fri, 02 Feb 2001 22:19:02 +0100] rev 11033
split = split_conv (for compatibility);
wenzelm [Fri, 02 Feb 2001 22:18:10 +0100] rev 11032
added hidden internal_split constant;
tuned;
wenzelm [Fri, 02 Feb 2001 22:17:31 +0100] rev 11031
isatool convert;
paulson [Fri, 02 Feb 2001 11:42:36 +0100] rev 11030
new theorem fib_mult_eq_setsum
oheimb [Fri, 02 Feb 2001 00:31:39 +0100] rev 11029
little bugfixes; added induct_thm_tac
wenzelm [Thu, 01 Feb 2001 21:28:23 +0100] rev 11028
moved to Product_Type_lemmas.ML
oheimb [Thu, 01 Feb 2001 20:56:21 +0100] rev 11027
added translations for bind_thm and val
oheimb [Thu, 01 Feb 2001 20:53:13 +0100] rev 11026
converted to Isar, simplifying recursion on class hierarchy
oheimb [Thu, 01 Feb 2001 20:51:48 +0100] rev 11025
converted to Isar therory, adding attributes complete_split and split_format
wenzelm [Thu, 01 Feb 2001 20:51:13 +0100] rev 11024
converted to new-style theories;
wenzelm [Thu, 01 Feb 2001 20:48:58 +0100] rev 11023
updated
wenzelm [Thu, 01 Feb 2001 20:45:54 +0100] rev 11022
ext_classrel: certify_class;
wenzelm [Thu, 01 Feb 2001 20:45:11 +0100] rev 11021
comment
wenzelm [Thu, 01 Feb 2001 20:44:19 +0100] rev 11020
tuned
wenzelm [Thu, 01 Feb 2001 20:43:59 +0100] rev 11019
tuned;
wenzelm [Thu, 01 Feb 2001 20:43:41 +0100] rev 11018
added "numerals" theorems;
wenzelm [Thu, 01 Feb 2001 20:43:14 +0100] rev 11017
thms_containing: term args;
wenzelm [Thu, 01 Feb 2001 20:42:34 +0100] rev 11016
* Pure: 'thms_containing' now takes actual terms as arguments;
* isatool convert assists in eliminating legacy ML scripts;
oheimb [Thu, 01 Feb 2001 18:47:31 +0100] rev 11015
added sum_case_map_upd_empty, sum_case_empty_map_upd, and
sum_case_map_upd_map_upd (also to default simpset),
added map_of_map
oheimb [Thu, 01 Feb 2001 18:13:06 +0100] rev 11014
debugged declare
oheimb [Thu, 01 Feb 2001 17:03:19 +0100] rev 11013
further minor improvements
wenzelm [Wed, 31 Jan 2001 22:16:22 +0100] rev 11012
strip_blanks moved to General/symbol.ML;
wenzelm [Wed, 31 Jan 2001 22:15:53 +0100] rev 11011
pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm [Wed, 31 Jan 2001 22:14:53 +0100] rev 11010
added strip_blanks;
oheimb [Wed, 31 Jan 2001 16:35:46 +0100] rev 11009
added attribute declarations, etc.
oheimb [Wed, 31 Jan 2001 10:15:55 +0100] rev 11008
improved theory reference in comment
oheimb [Wed, 31 Jan 2001 10:15:01 +0100] rev 11007
added diff_single_insert and subset_image_iff
oheimb [Wed, 31 Jan 2001 10:13:22 +0100] rev 11006
shortened proof of some1_equality
wenzelm [Wed, 31 Jan 2001 01:13:01 +0100] rev 11005
more robust handling of rule cases hints;
wenzelm [Tue, 30 Jan 2001 23:53:46 +0100] rev 11004
tuned;
oheimb [Tue, 30 Jan 2001 18:57:24 +0100] rev 11003
added if_def2
oheimb [Tue, 30 Jan 2001 18:53:46 +0100] rev 11002
added foldln
oheimb [Tue, 30 Jan 2001 18:48:33 +0100] rev 11001
corrected file name suffixes
oheimb [Tue, 30 Jan 2001 18:47:00 +0100] rev 11000
removed (obsolete) mult_assumption
berghofe [Tue, 30 Jan 2001 14:48:27 +0100] rev 10999
Fixed bug in complete_split_rule_var.
wenzelm [Tue, 30 Jan 2001 14:21:50 +0100] rev 10998
tuned;
wenzelm [Mon, 29 Jan 2001 23:54:56 +0100] rev 10997
avoid dead code;
nipkow [Mon, 29 Jan 2001 23:02:21 +0100] rev 10996
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow [Mon, 29 Jan 2001 22:25:45 +0100] rev 10995
*** empty log message ***
nipkow [Mon, 29 Jan 2001 19:24:17 +0100] rev 10994
*** empty log message ***
wenzelm [Mon, 29 Jan 2001 18:56:37 +0100] rev 10993
added Unix example;
wenzelm [Mon, 29 Jan 2001 14:14:17 +0100] rev 10992
updated;
wenzelm [Mon, 29 Jan 2001 14:14:03 +0100] rev 10991
*** empty log message ***
berghofe [Mon, 29 Jan 2001 13:31:30 +0100] rev 10990
Completely split rule eval_evals_exec.induct before applying it.
berghofe [Mon, 29 Jan 2001 13:28:15 +0100] rev 10989
New function complete_split_rule for complete splitting of partially
splitted rules (as generated by inductive definition package).
berghofe [Mon, 29 Jan 2001 13:26:04 +0100] rev 10988
Splitting of arguments of product types in induction rules is now less
aggressive.
paulson [Mon, 29 Jan 2001 10:28:00 +0100] rev 10987
fixed the pr example
paulson [Mon, 29 Jan 2001 10:27:29 +0100] rev 10986
simplified gcd
nipkow [Sun, 28 Jan 2001 16:46:19 +0100] rev 10985
fixed set comprehension print translation
nipkow [Fri, 26 Jan 2001 15:50:52 +0100] rev 10984
Merged Example into While_Combi
nipkow [Fri, 26 Jan 2001 15:50:28 +0100] rev 10983
*** empty log message ***
wenzelm [Fri, 26 Jan 2001 15:02:04 +0100] rev 10982
renamed to Transitive_Closure_lemmas.ML;
wenzelm [Fri, 26 Jan 2001 00:19:50 +0100] rev 10981
tuned;
wenzelm [Fri, 26 Jan 2001 00:15:36 +0100] rev 10980
Transitive_Closure turned into new-style theory;
wenzelm [Fri, 26 Jan 2001 00:14:25 +0100] rev 10979
tuned;
nipkow [Thu, 25 Jan 2001 15:31:31 +0100] rev 10978
*** empty log message ***
kleing [Thu, 25 Jan 2001 11:59:52 +0100] rev 10977
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
Verificard
wenzelm [Wed, 24 Jan 2001 21:01:47 +0100] rev 10976
* Document preparation: renamed standard symbols \<ll> to \<lless> and
\<gg> to \<ggreater>;
wenzelm [Wed, 24 Jan 2001 20:57:19 +0100] rev 10975
added eufrak symbols;
renamed \<ll> to \<lless> and \<gg> to \<ggreater>;
wenzelm [Wed, 24 Jan 2001 20:56:12 +0100] rev 10974
more symbols;
wenzelm [Wed, 24 Jan 2001 20:55:29 +0100] rev 10973
empty_upd_none;
oheimb [Wed, 24 Jan 2001 17:53:01 +0100] rev 10972
debugging and extensions
nipkow [Wed, 24 Jan 2001 12:29:10 +0100] rev 10971
*** empty log message ***
nipkow [Wed, 24 Jan 2001 11:59:15 +0100] rev 10970
*** empty log message ***
wenzelm [Wed, 24 Jan 2001 00:06:32 +0100] rev 10969
no_brackets;
wenzelm [Tue, 23 Jan 2001 18:17:14 +0100] rev 10968
tuned;
paulson [Tue, 23 Jan 2001 18:13:00 +0100] rev 10967
arg_cong, tacticals, pr, defer, prefer
wenzelm [Tue, 23 Jan 2001 18:05:53 +0100] rev 10966
added HOL-Unix example;
paulson [Tue, 23 Jan 2001 15:48:35 +0100] rev 10965
2 to #2
paulson [Tue, 23 Jan 2001 15:47:36 +0100] rev 10964
the 0<n premise was unnecessary
paulson [Tue, 23 Jan 2001 15:46:25 +0100] rev 10963
added a "pr" example; tidied
paulson [Mon, 22 Jan 2001 17:26:19 +0100] rev 10962
deleted several obsolete lemmas from NatArith.ML
paulson [Mon, 22 Jan 2001 11:46:25 +0100] rev 10961
tidied using arith_tac
paulson [Mon, 22 Jan 2001 11:45:57 +0100] rev 10960
deleted obsolete theorems
paulson [Mon, 22 Jan 2001 11:45:29 +0100] rev 10959
tided
paulson [Mon, 22 Jan 2001 11:02:53 +0100] rev 10958
arg_cong example; tidying to use @subgoals
paulson [Mon, 22 Jan 2001 11:01:49 +0100] rev 10957
rename_tac example; tidying to use @subgoals
paulson [Mon, 22 Jan 2001 11:01:05 +0100] rev 10956
new examples theory Rules/Tacticals.thy
wenzelm [Sun, 21 Jan 2001 19:55:25 +0100] rev 10955
setuo indent: \isaindent;
wenzelm [Sun, 21 Jan 2001 19:54:52 +0100] rev 10954
setup indent;
wenzelm [Sun, 21 Jan 2001 19:54:05 +0100] rev 10953
added spaces;
added default_indent, indent;
wenzelm [Sun, 21 Jan 2001 19:53:29 +0100] rev 10952
support general indentation (e.g. for non-tt latex output);
tuned;
wenzelm [Sun, 21 Jan 2001 19:52:32 +0100] rev 10951
added replicate_string;
wenzelm [Sun, 21 Jan 2001 19:50:43 +0100] rev 10950
updated;
wenzelm [Sun, 21 Jan 2001 13:21:14 +0100] rev 10949
\isaindent;
wenzelm [Sat, 20 Jan 2001 00:35:35 +0100] rev 10948
tuned;
wenzelm [Sat, 20 Jan 2001 00:35:10 +0100] rev 10947
Ring_and_Field_Example;
wenzelm [Sat, 20 Jan 2001 00:34:46 +0100] rev 10946
instance int :: ordered_ring moved to Ring_and_Field_Example, because
it changes the way that int expressions get simplified, violating
the strict library principle (cf. README.html);
wenzelm [Sat, 20 Jan 2001 00:32:56 +0100] rev 10945
added Library/Ring_and_Field_Example.thy;
wenzelm [Sat, 20 Jan 2001 00:01:40 +0100] rev 10944
*** empty log message ***
wenzelm [Fri, 19 Jan 2001 23:53:07 +0100] rev 10943
added HOL/Library/Nested_Environment.thy;
wenzelm [Fri, 19 Jan 2001 23:28:50 +0100] rev 10942
updated;
wenzelm [Fri, 19 Jan 2001 19:26:02 +0100] rev 10941
more bugs;
wenzelm [Fri, 19 Jan 2001 13:35:11 +0100] rev 10940
forget RPM;
wenzelm [Fri, 19 Jan 2001 11:53:21 +0100] rev 10939
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm [Thu, 18 Jan 2001 21:41:36 +0100] rev 10938
made SML/XL happy;
wenzelm [Thu, 18 Jan 2001 20:40:47 +0100] rev 10937
tuned;
wenzelm [Thu, 18 Jan 2001 20:40:33 +0100] rev 10936
show(_i): check goal;
wenzelm [Thu, 18 Jan 2001 20:39:53 +0100] rev 10935
show/thus: check_goal;
wenzelm [Thu, 18 Jan 2001 20:38:58 +0100] rev 10934
show/thus: Toplevel.proof';
wenzelm [Thu, 18 Jan 2001 20:38:32 +0100] rev 10933
infix \\\\;
wenzelm [Thu, 18 Jan 2001 20:37:38 +0100] rev 10932
added exists_stamp;
added PureN, CPureN;
wenzelm [Thu, 18 Jan 2001 20:36:57 +0100] rev 10931
use Sign.PureN, Sign.CPureN;
wenzelm [Thu, 18 Jan 2001 20:36:31 +0100] rev 10930
Sign.exists_stamp;
wenzelm [Thu, 18 Jan 2001 20:36:08 +0100] rev 10929
tuned \<And> and \<Or>;
wenzelm [Thu, 18 Jan 2001 20:35:39 +0100] rev 10928
generate index.html for pdf docs;
oheimb [Thu, 18 Jan 2001 20:23:51 +0100] rev 10927
splitted Loop rule
paulson [Thu, 18 Jan 2001 18:39:43 +0100] rev 10926
removed redundant proof
oheimb [Thu, 18 Jan 2001 17:38:56 +0100] rev 10925
is_class and class now as defs (rather than translations); corrected Digest.thy
wenzelm [Tue, 16 Jan 2001 21:54:43 +0100] rev 10924
use_output: proper handling of non-ASCII symbols;
wenzelm [Tue, 16 Jan 2001 21:53:57 +0100] rev 10923
export plain_output;
kleing [Tue, 16 Jan 2001 19:22:13 +0100] rev 10922
Store.thy is obsolete (newref isn't used any more)
kleing [Tue, 16 Jan 2001 19:21:21 +0100] rev 10921
removed obsolete MicroJava/JVM/Store.thy
kleing [Tue, 16 Jan 2001 15:56:34 +0100] rev 10920
newref -> new_Addr
paulson [Tue, 16 Jan 2001 12:20:52 +0100] rev 10919
renamings: real_of_nat, real_of_int -> (overloaded) real
inf_close -> approx
SReal -> Reals
SNat -> Nats
wenzelm [Tue, 16 Jan 2001 00:40:57 +0100] rev 10918
renamed Product_Type.split to split_conv;
wenzelm [Tue, 16 Jan 2001 00:38:59 +0100] rev 10917
use Syntax.read_xnum;
wenzelm [Tue, 16 Jan 2001 00:38:25 +0100] rev 10916
tuned examples;
wenzelm [Tue, 16 Jan 2001 00:37:41 +0100] rev 10915
* HOL/datatype: induction rule for arbitrarily branching datatypes is
now expressed as a proper nested rule (old-style tactic scripts may
require atomize_strip_tac to cope with non-atomic premises);
* HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
to "split_conv" (old name still available for compatibility);
* HOL: improved concrete syntax for strings (e.g. allows translation
rules with string literals);
wenzelm [Tue, 16 Jan 2001 00:35:50 +0100] rev 10914
use_text etc.: proper output of error messages;
wenzelm [Tue, 16 Jan 2001 00:35:18 +0100] rev 10913
export fold_ast etc.;
wenzelm [Tue, 16 Jan 2001 00:34:31 +0100] rev 10912
removed Session.finish ();
wenzelm [Tue, 16 Jan 2001 00:33:40 +0100] rev 10911
proper induction rule for arbitrarily branching datatype;
wenzelm [Tue, 16 Jan 2001 00:32:38 +0100] rev 10910
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm [Tue, 16 Jan 2001 00:30:06 +0100] rev 10909
improved string syntax (allow translation rules);
wenzelm [Tue, 16 Jan 2001 00:29:43 +0100] rev 10908
renamed Abs_Node_inject to Abs_Node_inj;
wenzelm [Tue, 16 Jan 2001 00:29:12 +0100] rev 10907
added atomize_strip_tac;
wenzelm [Tue, 16 Jan 2001 00:28:50 +0100] rev 10906
tuned atomize;
wenzelm [Tue, 16 Jan 2001 00:27:37 +0100] rev 10905
-f option;
wenzelm [Tue, 16 Jan 2001 00:25:54 +0100] rev 10904
removed;
wenzelm [Tue, 16 Jan 2001 00:25:25 +0100] rev 10903
removed ex/StringEx.ML;
wenzelm [Tue, 16 Jan 2001 00:25:00 +0100] rev 10902
split_conv;
wenzelm [Tue, 16 Jan 2001 00:24:36 +0100] rev 10901
updated;
wenzelm [Tue, 16 Jan 2001 00:23:14 +0100] rev 10900
isabelle -f;
wenzelm [Tue, 16 Jan 2001 00:22:43 +0100] rev 10899
more method_setup examples;
paulson [Mon, 15 Jan 2001 10:29:13 +0100] rev 10898
lcp's pass over the book, chapters 1-8
kleing [Sun, 14 Jan 2001 18:19:18 +0100] rev 10897
removed instructions Aconst_null+Bipush, introduced LitPush
kleing [Sun, 14 Jan 2001 18:17:37 +0100] rev 10896
tuned
nipkow [Sun, 14 Jan 2001 14:12:42 +0100] rev 10895
*** empty log message ***
wenzelm [Fri, 12 Jan 2001 20:04:41 +0100] rev 10894
use_text_verbose: priority output;
wenzelm [Fri, 12 Jan 2001 20:04:22 +0100] rev 10893
use_mltext: priority output;
wenzelm [Fri, 12 Jan 2001 20:04:00 +0100] rev 10892
HOLogic.dest_binum;
avoid handle _ !!!
wenzelm [Fri, 12 Jan 2001 20:03:26 +0100] rev 10891
hide dest_bin;
wenzelm [Fri, 12 Jan 2001 20:03:04 +0100] rev 10890
HOLogic.dest_binum;
paulson [Fri, 12 Jan 2001 18:00:40 +0100] rev 10889
wrong font for braces
paulson [Fri, 12 Jan 2001 18:00:12 +0100] rev 10888
LateX-2e moans about using \\choose
paulson [Fri, 12 Jan 2001 17:59:37 +0100] rev 10887
the \\epsilon character causes font errors in a section title
wenzelm [Fri, 12 Jan 2001 16:56:20 +0100] rev 10886
made SML/NJ happy;
paulson [Fri, 12 Jan 2001 16:32:01 +0100] rev 10885
lcp's pass over the book, chapters 1-8
paulson [Fri, 12 Jan 2001 16:28:14 +0100] rev 10884
renaming of some files
paulson [Fri, 12 Jan 2001 16:19:44 +0100] rev 10883
updated for new version of even-examples.tex
paulson [Fri, 12 Jan 2001 16:16:09 +0100] rev 10882
updated for new version of advanced-examples.tex
paulson [Fri, 12 Jan 2001 16:11:55 +0100] rev 10881
abs and other small changes
paulson [Fri, 12 Jan 2001 16:10:56 +0100] rev 10880
updated for new version of numerics.tex
paulson [Fri, 12 Jan 2001 16:09:33 +0100] rev 10879
renaming to avoid clashes
paulson [Fri, 12 Jan 2001 16:07:20 +0100] rev 10878
auto update
paulson [Fri, 12 Jan 2001 16:05:12 +0100] rev 10877
general revisions
wenzelm [Fri, 12 Jan 2001 11:08:06 +0100] rev 10876
added Sigma_Algebra;
wenzelm [Fri, 12 Jan 2001 11:06:50 +0100] rev 10875
added Induct/Sigma_Algebra.thy;
wenzelm [Fri, 12 Jan 2001 09:32:53 +0100] rev 10874
tuned;
wenzelm [Thu, 11 Jan 2001 21:51:14 +0100] rev 10873
do not hilite "xnum";
wenzelm [Thu, 11 Jan 2001 19:38:37 +0100] rev 10872
make_raw: do not AutoBind.drop_judgment;
wenzelm [Thu, 11 Jan 2001 19:38:02 +0100] rev 10871
induct cases: RuleCases.make_raw;
wenzelm [Thu, 11 Jan 2001 19:37:46 +0100] rev 10870
added strict_prefixI', strict_prefixE';
wenzelm [Thu, 11 Jan 2001 19:36:25 +0100] rev 10869
subst syntax;
nipkow [Thu, 11 Jan 2001 12:49:48 +0100] rev 10868
*** empty log message ***
paulson [Thu, 11 Jan 2001 12:12:01 +0100] rev 10867
lcp's suggestions for CTL
nipkow [Thu, 11 Jan 2001 11:47:57 +0100] rev 10866
*** empty log message ***
paulson [Thu, 11 Jan 2001 11:37:03 +0100] rev 10865
a new label
paulson [Thu, 11 Jan 2001 11:35:39 +0100] rev 10864
revisions corresponding to the new version of sets.tex
nipkow [Wed, 10 Jan 2001 20:41:14 +0100] rev 10863
Added <cdot> syntax for continuous application $.
wenzelm [Wed, 10 Jan 2001 20:21:11 +0100] rev 10862
isatool unsymbolize;
wenzelm [Wed, 10 Jan 2001 20:20:10 +0100] rev 10861
updated;
wenzelm [Wed, 10 Jan 2001 20:19:56 +0100] rev 10860
tuned \DOT, \DDOT;
wenzelm [Wed, 10 Jan 2001 20:19:34 +0100] rev 10859
added \<wrong> symbol;
wenzelm [Wed, 10 Jan 2001 20:18:55 +0100] rev 10858
tuned;
paulson [Wed, 10 Jan 2001 17:21:31 +0100] rev 10857
revisions e.g. images, transitive closure...
nipkow [Wed, 10 Jan 2001 13:30:25 +0100] rev 10856
*** empty log message ***
nipkow [Wed, 10 Jan 2001 12:53:50 +0100] rev 10855
*** empty log message ***
paulson [Wed, 10 Jan 2001 12:43:51 +0100] rev 10854
case_tac on bools
paulson [Wed, 10 Jan 2001 12:43:40 +0100] rev 10853
case_tac subgoals
paulson [Wed, 10 Jan 2001 11:16:38 +0100] rev 10852
deleted the obsolete nat_neqE (and reformatting)
paulson [Wed, 10 Jan 2001 11:15:24 +0100] rev 10851
deleted the obsolete nat_neqE
paulson [Wed, 10 Jan 2001 11:14:30 +0100] rev 10850
generalizing the LEAST theorems from "nat" to linear
orderings and wellorderings
paulson [Wed, 10 Jan 2001 11:13:11 +0100] rev 10849
now using "by" for one-line proofs
paulson [Wed, 10 Jan 2001 11:12:45 +0100] rev 10848
various changes including the SOME examples, rule_format and "by"
paulson [Wed, 10 Jan 2001 11:12:17 +0100] rev 10847
loads the new theory
paulson [Wed, 10 Jan 2001 11:09:11 +0100] rev 10846
reformatting, and splitting the end of "Primes" to create "Forward"
nipkow [Wed, 10 Jan 2001 11:08:29 +0100] rev 10845
*** empty log message ***
paulson [Wed, 10 Jan 2001 11:07:11 +0100] rev 10844
now using "by" for one-line proofs
paulson [Wed, 10 Jan 2001 11:06:07 +0100] rev 10843
introduction of "by" and a few examples of SOME
paulson [Wed, 10 Jan 2001 11:05:27 +0100] rev 10842
auto update
paulson [Wed, 10 Jan 2001 11:05:13 +0100] rev 10841
new wfrec example
paulson [Wed, 10 Jan 2001 11:00:17 +0100] rev 10840
fixed the treatment of Rules and Sets
nipkow [Wed, 10 Jan 2001 10:40:34 +0100] rev 10839
*** empty log message ***
wenzelm [Wed, 10 Jan 2001 00:15:33 +0100] rev 10838
use \<acute>;
wenzelm [Wed, 10 Jan 2001 00:14:52 +0100] rev 10837
added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
wenzelm [Tue, 09 Jan 2001 23:48:30 +0100] rev 10836
added acute, cedilla, dieresis, hungarumlaut;
nipkow [Tue, 09 Jan 2001 15:36:30 +0100] rev 10835
` -> $
nipkow [Tue, 09 Jan 2001 15:32:27 +0100] rev 10834
*** empty log message ***
nipkow [Tue, 09 Jan 2001 15:29:17 +0100] rev 10833
`` -> ` and ``` -> ``
nipkow [Tue, 09 Jan 2001 15:22:13 +0100] rev 10832
`` -> and ``` -> ``
wenzelm [Tue, 09 Jan 2001 15:18:07 +0100] rev 10831
replaced \<macron> by \<inverse>;
wenzelm [Tue, 09 Jan 2001 15:17:08 +0100] rev 10830
avoid renaming of params in cases;
wenzelm [Tue, 09 Jan 2001 15:15:28 +0100] rev 10829
split_all operation;
oheimb [Tue, 09 Jan 2001 13:54:44 +0100] rev 10828
improved evaluation judgment syntax; modified Loop rule
wenzelm [Tue, 09 Jan 2001 12:11:56 +0100] rev 10827
syntax (xsymbols);
nipkow [Mon, 08 Jan 2001 12:27:36 +0100] rev 10826
Removed Applyall
paulson [Mon, 08 Jan 2001 11:06:24 +0100] rev 10825
additional pattern allows reduction of fractions to lowest terms
nipkow [Mon, 08 Jan 2001 10:33:51 +0100] rev 10824
*** empty log message ***
wenzelm [Sun, 07 Jan 2001 22:39:28 +0100] rev 10823
updated;
wenzelm [Sun, 07 Jan 2001 21:45:14 +0100] rev 10822
removed ID (avoid CVS conflicts with generated versions);
wenzelm [Sun, 07 Jan 2001 21:41:56 +0100] rev 10821
CHANGED_PROP;
wenzelm [Sun, 07 Jan 2001 21:40:49 +0100] rev 10820
removed MicroJava/BV/Convert.thy;
wenzelm [Sun, 07 Jan 2001 21:37:40 +0100] rev 10819
do not AutoBind.drop_judgment;
wenzelm [Sun, 07 Jan 2001 21:36:59 +0100] rev 10818
tuned output;
wenzelm [Sun, 07 Jan 2001 21:36:11 +0100] rev 10817
tuned norm_hhf(_tac);
wenzelm [Sun, 07 Jan 2001 21:35:34 +0100] rev 10816
added is_norm_hhf;
wenzelm [Sun, 07 Jan 2001 21:35:11 +0100] rev 10815
removed outdated comment;
wenzelm [Sun, 07 Jan 2001 21:34:45 +0100] rev 10814
case binds: AutoBind.drop_judgment;
wenzelm [Sun, 07 Jan 2001 21:34:16 +0100] rev 10813
tuned split_all_tac;
kleing [Sun, 07 Jan 2001 18:43:13 +0100] rev 10812
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
wenzelm [Sat, 06 Jan 2001 21:31:37 +0100] rev 10811
support ?case binding;
tuned;
wenzelm [Sat, 06 Jan 2001 21:31:09 +0100] rev 10810
apply_case: more robust handling of bounds;
moved norm_hhf to Pure/tactic.ML;
wenzelm [Sat, 06 Jan 2001 21:29:29 +0100] rev 10809
moved norm_hhf_tac to Pure/tactic.ML;
adapted invoke_case;
wenzelm [Sat, 06 Jan 2001 21:28:30 +0100] rev 10808
added drop_judgment;
wenzelm [Sat, 06 Jan 2001 21:28:04 +0100] rev 10807
export read_inst', inst';
tuned;
wenzelm [Sat, 06 Jan 2001 21:27:33 +0100] rev 10806
added list_abs;
wenzelm [Sat, 06 Jan 2001 21:27:12 +0100] rev 10805
added norm_hhf(_tac);
wenzelm [Sat, 06 Jan 2001 21:26:27 +0100] rev 10804
Tactic.norm_hhf;
wenzelm [Sat, 06 Jan 2001 21:26:13 +0100] rev 10803
'of:' params spec;
tuned;
wenzelm [Sat, 06 Jan 2001 21:22:35 +0100] rev 10802
'cases' / 'induct' method: ?case binding, 'of:' spec;
nipkow [Sat, 06 Jan 2001 12:39:05 +0100] rev 10801
*** empty log message ***
nipkow [Sat, 06 Jan 2001 11:27:09 +0100] rev 10800
*** empty log message ***
nipkow [Sat, 06 Jan 2001 10:36:19 +0100] rev 10799
*** empty log message ***
nipkow [Fri, 05 Jan 2001 18:49:16 +0100] rev 10798
*** empty log message ***
nipkow [Fri, 05 Jan 2001 18:48:18 +0100] rev 10797
^^ -> ```
Univalent -> single_valued
paulson [Fri, 05 Jan 2001 18:33:47 +0100] rev 10796
Fleuriot reference
paulson [Fri, 05 Jan 2001 18:32:57 +0100] rev 10795
minor edits to Chapters 1-3
paulson [Fri, 05 Jan 2001 18:32:33 +0100] rev 10794
revisions especially concerning the reals
nipkow [Fri, 05 Jan 2001 18:31:48 +0100] rev 10793
*** empty log message ***
paulson [Fri, 05 Jan 2001 18:16:01 +0100] rev 10792
a few extra brackets
nipkow [Fri, 05 Jan 2001 15:39:34 +0100] rev 10791
*** empty log message ***
nipkow [Fri, 05 Jan 2001 15:16:40 +0100] rev 10790
*** empty log message ***
nipkow [Fri, 05 Jan 2001 14:28:10 +0100] rev 10789
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow [Fri, 05 Jan 2001 13:10:37 +0100] rev 10788
*** empty log message ***
paulson [Fri, 05 Jan 2001 10:19:32 +0100] rev 10787
new UNITY examples by Sidi Ehmety
paulson [Fri, 05 Jan 2001 10:19:14 +0100] rev 10786
Field of a relation, and some Domain/Range rules
paulson [Fri, 05 Jan 2001 10:18:46 +0100] rev 10785
finite_trancl: new theorem by Sidi Ehmety
paulson [Fri, 05 Jan 2001 10:17:48 +0100] rev 10784
more removal of obsolete rules
paulson [Fri, 05 Jan 2001 10:17:19 +0100] rev 10783
fixed two proofs that were affected by the removal of obsolete rules
paulson [Fri, 05 Jan 2001 10:15:48 +0100] rev 10782
new examples by Sidi Ehmety
wenzelm [Thu, 04 Jan 2001 19:41:13 +0100] rev 10781
tuned comment;