Wed, 24 Jul 2002 00:11:24 +0200 wenzelm adapted fact names;
Wed, 24 Jul 2002 00:10:52 +0200 wenzelm predicate defs via locales;
Wed, 24 Jul 2002 00:09:44 +0200 wenzelm locales: predicate defs;
Wed, 24 Jul 2002 00:08:52 +0200 wenzelm * Pure: locale specifications now produce predicate definitions;
Tue, 23 Jul 2002 15:07:12 +0200 paulson Relativization and Separation for the function "nth"
Mon, 22 Jul 2002 13:55:44 +0200 berghofe Added "nocite" to avoid BibTeX error when proofs are switched off.
Sun, 21 Jul 2002 15:52:39 +0200 berghofe Added program extraction keywords.
Sun, 21 Jul 2002 15:45:41 +0200 berghofe Document for program extraction in HOL.
Sun, 21 Jul 2002 15:44:42 +0200 berghofe Examples for program extraction in HOL.
Sun, 21 Jul 2002 15:43:14 +0200 berghofe Rules for rewriting HOL proofs.
Sun, 21 Jul 2002 15:42:30 +0200 berghofe Added theory for setting up program extraction.
Sun, 21 Jul 2002 15:37:04 +0200 berghofe Added program extraction module.
Fri, 19 Jul 2002 18:44:37 +0200 wenzelm *** empty log message ***
Fri, 19 Jul 2002 18:44:36 +0200 wenzelm accomodate cumulative locale predicates;
Fri, 19 Jul 2002 18:44:07 +0200 wenzelm support locale ``views'' (for cumulative predicates);
Fri, 19 Jul 2002 18:06:31 +0200 paulson Towards relativization and absoluteness of formula_rec
Fri, 19 Jul 2002 13:29:22 +0200 paulson Absoluteness of the function "nth"
Fri, 19 Jul 2002 13:28:19 +0200 paulson A couple of new theorems for Constructible
Thu, 18 Jul 2002 15:21:42 +0200 paulson absoluteness for "formula" and "eclose"
Thu, 18 Jul 2002 12:10:24 +0200 wenzelm define cumulative predicate view;
Thu, 18 Jul 2002 12:09:44 +0200 wenzelm adapted add_locale;
Thu, 18 Jul 2002 12:09:28 +0200 wenzelm adapted locale syntax;
Thu, 18 Jul 2002 12:09:08 +0200 wenzelm fixed inform_file_retracted: remove_thy;
Thu, 18 Jul 2002 12:08:45 +0200 wenzelm ACe_axioms;
Thu, 18 Jul 2002 12:05:51 +0200 wenzelm added satisfy_hyps;
Thu, 18 Jul 2002 12:05:29 +0200 wenzelm quantify LC (conflict with const name of HOL);
Thu, 18 Jul 2002 10:37:55 +0200 paulson new theorems to support Constructible proofs
Wed, 17 Jul 2002 16:41:32 +0200 paulson Formulas (and lists) in M (and L!)
Wed, 17 Jul 2002 15:48:54 +0200 paulson Expressing Lset and L without using length and arity; simplifies Separation
Tue, 16 Jul 2002 20:25:21 +0200 schirmer Added conditional and (&&) and or (||).
Tue, 16 Jul 2002 18:52:26 +0200 wenzelm adapted locales;
Tue, 16 Jul 2002 18:46:59 +0200 wenzelm adapted locales;
Tue, 16 Jul 2002 18:46:13 +0200 wenzelm tuned;
Tue, 16 Jul 2002 18:46:04 +0200 wenzelm adapted locales;
Tue, 16 Jul 2002 18:43:05 +0200 wenzelm rearranged to work without proof contexts;
Tue, 16 Jul 2002 18:42:07 +0200 wenzelm export_standard supercedes export_single;
Tue, 16 Jul 2002 18:41:50 +0200 wenzelm export map_context;
Tue, 16 Jul 2002 18:41:18 +0200 wenzelm assert_propT;
Tue, 16 Jul 2002 18:41:00 +0200 wenzelm proper predicate definitions of locale body;
Tue, 16 Jul 2002 18:40:11 +0200 wenzelm add_locale: adapted args;
Tue, 16 Jul 2002 18:39:55 +0200 wenzelm locale: optional predicate name, or "open";
Tue, 16 Jul 2002 18:39:27 +0200 wenzelm module now right after ProofContext (for locales);
Tue, 16 Jul 2002 18:38:36 +0200 wenzelm avoid "_st" versions of proof data;
Tue, 16 Jul 2002 18:38:11 +0200 wenzelm context rules;
Tue, 16 Jul 2002 18:37:56 +0200 wenzelm tuned order of modules;
Tue, 16 Jul 2002 18:37:03 +0200 wenzelm added equal_elim_rule1;
Tue, 16 Jul 2002 18:26:52 +0200 wenzelm moved stuff to List.thy;
Tue, 16 Jul 2002 18:26:36 +0200 wenzelm moved stuff from Main.thy;
Tue, 16 Jul 2002 18:26:09 +0200 wenzelm adapted to locale defs;
Tue, 16 Jul 2002 18:25:48 +0200 wenzelm updated;
Tue, 16 Jul 2002 16:29:36 +0200 paulson instantiation of locales M_trancl and M_wfrank;
Tue, 16 Jul 2002 16:28:49 +0200 paulson tweaked definition of setclass
Tue, 16 Jul 2002 16:28:26 +0200 paulson new lemmas
Tue, 16 Jul 2002 09:36:11 +0200 nipkow *** empty log message ***
Mon, 15 Jul 2002 15:28:51 +0200 isatest mail address update
Mon, 15 Jul 2002 10:41:34 +0200 schirmer fix latex output
Sun, 14 Jul 2002 19:59:55 +0200 paulson Removal of mono.thy
Sun, 14 Jul 2002 15:14:43 +0200 paulson improved presentation markup
Sun, 14 Jul 2002 15:11:21 +0200 paulson merged Update with func
Fri, 12 Jul 2002 17:16:22 +0200 schirmer little Bugfix
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip