2002-08-13 *** empty log message ***
nipkow [Tue, 13 Aug 2002 21:54:23 +0200] rev 13497
*** empty log message ***
2002-08-13 In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson [Tue, 13 Aug 2002 17:42:34 +0200] rev 13496
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to the new theory Internalize.thy
2002-08-13 more robust printing of numerals;
wenzelm [Tue, 13 Aug 2002 12:16:14 +0200] rev 13495
more robust printing of numerals;
2002-08-13 new file Constructible/Satisfies_absolute.thy
paulson [Tue, 13 Aug 2002 11:03:11 +0200] rev 13494
new file Constructible/Satisfies_absolute.thy
2002-08-12 Lots of new results concerning recursive datatypes, towards absoluteness of
paulson [Mon, 12 Aug 2002 18:01:44 +0200] rev 13493
Lots of new results concerning recursive datatypes, towards absoluteness of "satisfies"
2002-08-12 *** empty log message ***
nipkow [Mon, 12 Aug 2002 17:59:57 +0200] rev 13492
*** empty log message ***
2002-08-12 *** empty log message ***
nipkow [Mon, 12 Aug 2002 17:48:19 +0200] rev 13491
*** empty log message ***
2002-08-12 Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow [Mon, 12 Aug 2002 17:48:15 +0200] rev 13490
Added Mi and Max on sets, hid Min and Pls on numerals.
2002-08-09 *** empty log message ***
nipkow [Fri, 09 Aug 2002 11:22:18 +0200] rev 13489
*** empty log message ***
2002-08-08 transform_error: pass through Interrupt;
wenzelm [Thu, 08 Aug 2002 23:53:22 +0200] rev 13488
transform_error: pass through Interrupt;
2002-08-08 tuned;
wenzelm [Thu, 08 Aug 2002 23:52:55 +0200] rev 13487
tuned;
2002-08-08 exception SIMPROC_FAIL: solid error reporting of simprocs;
wenzelm [Thu, 08 Aug 2002 23:51:24 +0200] rev 13486
exception SIMPROC_FAIL: solid error reporting of simprocs;
2002-08-08 tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm [Thu, 08 Aug 2002 23:50:23 +0200] rev 13485
tuned prove_conv (error reporting done within meta_simplifier.ML);
2002-08-08 adhoc_freeze_vars;
wenzelm [Thu, 08 Aug 2002 23:49:44 +0200] rev 13484
adhoc_freeze_vars;
2002-08-08 proper instantiation of mk_left_commute;
wenzelm [Thu, 08 Aug 2002 23:48:31 +0200] rev 13483
proper instantiation of mk_left_commute;
2002-08-08 converted;
wenzelm [Thu, 08 Aug 2002 23:47:41 +0200] rev 13482
converted;
2002-08-08 tuned deps;
wenzelm [Thu, 08 Aug 2002 23:46:51 +0200] rev 13481
tuned deps;
2002-08-08 use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm [Thu, 08 Aug 2002 23:46:09 +0200] rev 13480
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
2002-08-08 Tactic.prove, Tactic.prove_standard;
wenzelm [Thu, 08 Aug 2002 23:42:49 +0200] rev 13479
Tactic.prove, Tactic.prove_standard;
2002-08-08 * Pure: improved error reporting of simprocs;
wenzelm [Thu, 08 Aug 2002 23:42:10 +0200] rev 13478
* Pure: improved error reporting of simprocs; tuned;
2002-08-07 tuned;
wenzelm [Wed, 07 Aug 2002 20:11:07 +0200] rev 13477
tuned;
2002-08-07 mk_left_commute: proper instantiation avoids expensive unification;
wenzelm [Wed, 07 Aug 2002 20:05:43 +0200] rev 13476
mk_left_commute: proper instantiation avoids expensive unification;
2002-08-07 tuned;
wenzelm [Wed, 07 Aug 2002 20:03:38 +0200] rev 13475
tuned;
2002-08-07 Simplifier.simproc(_i);
wenzelm [Wed, 07 Aug 2002 20:03:17 +0200] rev 13474
Simplifier.simproc(_i);
2002-08-07 Added time example at the end.
nipkow [Wed, 07 Aug 2002 18:32:50 +0200] rev 13473
Added time example at the end.
2002-08-07 section on "Rule declarations and methods";
wenzelm [Wed, 07 Aug 2002 17:36:05 +0200] rev 13472
section on "Rule declarations and methods";
2002-08-07 Removed (now unneeded) declaration of realizer for induction on datatype b.
berghofe [Wed, 07 Aug 2002 16:50:08 +0200] rev 13471
Removed (now unneeded) declaration of realizer for induction on datatype b.
2002-08-07 Removed (now unneeded) declarations of realizers for induction on lists and letters.
berghofe [Wed, 07 Aug 2002 16:49:25 +0200] rev 13470
Removed (now unneeded) declarations of realizers for induction on lists and letters.
2002-08-07 Added file Tools/datatype_realizer.ML
berghofe [Wed, 07 Aug 2002 16:48:20 +0200] rev 13469
Added file Tools/datatype_realizer.ML
2002-08-07 Removed (now unneeded) declaration of realizers for induction on natural numbers.
berghofe [Wed, 07 Aug 2002 16:47:36 +0200] rev 13468
Removed (now unneeded) declaration of realizers for induction on natural numbers.
2002-08-07 Module for defining realizers for induction and case analysis theorems
berghofe [Wed, 07 Aug 2002 16:46:15 +0200] rev 13467
Module for defining realizers for induction and case analysis theorems for datatypes.
2002-08-07 Added calls to add_dt_realizers.
berghofe [Wed, 07 Aug 2002 16:44:47 +0200] rev 13466
Added calls to add_dt_realizers.
2002-08-07 Exported function make_tnames.
berghofe [Wed, 07 Aug 2002 16:43:41 +0200] rev 13465
Exported function make_tnames.
2002-08-07 Fixed two bugs
nipkow [Wed, 07 Aug 2002 05:54:44 +0200] rev 13464
Fixed two bugs
2002-08-06 * Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm [Tue, 06 Aug 2002 11:24:27 +0200] rev 13463
* Provers: Simplifier.simproc(_i) now provide sane interface for setting up simprocs;
2002-08-06 sane interface for simprocs;
wenzelm [Tue, 06 Aug 2002 11:22:05 +0200] rev 13462
sane interface for simprocs;
2002-08-06 fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);
wenzelm [Tue, 06 Aug 2002 11:20:47 +0200] rev 13461
fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);
2002-08-06 predefined locales "var" and "struct" (useful for sharing parameters);
wenzelm [Tue, 06 Aug 2002 11:19:52 +0200] rev 13460
predefined locales "var" and "struct" (useful for sharing parameters);
2002-08-06 * Pure: predefined locales "var" and "struct" are useful for sharing
wenzelm [Tue, 06 Aug 2002 11:19:00 +0200] rev 13459
* Pure: predefined locales "var" and "struct" are useful for sharing parameters (as in CASL, for example); just specify something like ``var x + var y + struct M'' as import;
2002-08-05 protect simplifier operation against spurious exceptions from simprocs;
wenzelm [Mon, 05 Aug 2002 21:17:45 +0200] rev 13458
protect simplifier operation against spurious exceptions from simprocs;
2002-08-05 tuned;
wenzelm [Mon, 05 Aug 2002 21:17:04 +0200] rev 13457
tuned; subsection on simple meta-theory of structures;
2002-08-05 special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm [Mon, 05 Aug 2002 21:16:36 +0200] rev 13456
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
2002-08-05 Removed theory NatDef.
berghofe [Mon, 05 Aug 2002 14:35:33 +0200] rev 13455
Removed theory NatDef.
2002-08-05 Replaced nat_ind_tac by induct_tac.
berghofe [Mon, 05 Aug 2002 14:32:56 +0200] rev 13454
Replaced nat_ind_tac by induct_tac.
2002-08-05 Removed proof of Suc_le_D (already proved in Nat.thy).
berghofe [Mon, 05 Aug 2002 14:30:06 +0200] rev 13453
Removed proof of Suc_le_D (already proved in Nat.thy).
2002-08-05 Removed reference to theory NatDef.
berghofe [Mon, 05 Aug 2002 14:29:20 +0200] rev 13452
Removed reference to theory NatDef.
2002-08-05 Removed reference to simpset of NatDef.thy
berghofe [Mon, 05 Aug 2002 14:28:31 +0200] rev 13451
Removed reference to simpset of NatDef.thy
2002-08-05 Legacy ML bindings.
berghofe [Mon, 05 Aug 2002 14:27:55 +0200] rev 13450
Legacy ML bindings.
2002-08-05 - Converted to new theory format
berghofe [Mon, 05 Aug 2002 14:27:42 +0200] rev 13449
- Converted to new theory format - Moved NatDef stuff to theory Nat
2002-08-05 Moved NatDef stuff to theory Nat.
berghofe [Mon, 05 Aug 2002 14:26:54 +0200] rev 13448
Moved NatDef stuff to theory Nat.
2002-08-05 updated;
wenzelm [Mon, 05 Aug 2002 12:00:51 +0200] rev 13447
updated;
2002-08-02 added Isabelle LNCSes;
wenzelm [Fri, 02 Aug 2002 21:40:47 +0200] rev 13446
added Isabelle LNCSes;
2002-08-02 fixed long statement: P.opt_thm_name;
wenzelm [Fri, 02 Aug 2002 21:40:28 +0200] rev 13445
fixed long statement: P.opt_thm_name;
2002-08-02 fixed railroads;
wenzelm [Fri, 02 Aug 2002 17:52:51 +0200] rev 13444
fixed railroads;
2002-08-02 typedef: "open" option;
wenzelm [Fri, 02 Aug 2002 11:49:55 +0200] rev 13443
typedef: "open" option;
2002-08-02 declare projected "axioms" as "elim?";
wenzelm [Fri, 02 Aug 2002 11:12:34 +0200] rev 13442
declare projected "axioms" as "elim?";
(0) -10000 -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip