Mon, 04 Oct 1999 21:35:26 +0200 wenzelm added mk_conj, mk_disj, mk_imp;
Mon, 04 Oct 1999 21:34:20 +0200 wenzelm added BVC;
Mon, 04 Oct 1999 14:45:35 +0200 wenzelm added mk_conj, mk_disj, mk_imp;
Mon, 04 Oct 1999 13:47:28 +0200 paulson working snapshot (even Alloc)
Mon, 04 Oct 1999 13:45:31 +0200 paulson most results now refer to those for "extend"
Mon, 04 Oct 1999 12:22:14 +0200 wenzelm fixed lookup_theory;
Mon, 04 Oct 1999 10:19:18 +0200 paulson fixed CHANGED_GOAL, which is used by stac
Sun, 03 Oct 1999 15:54:25 +0200 wenzelm improved theory_source presentation (hook);
Sun, 03 Oct 1999 15:54:04 +0200 wenzelm improved theory_source presentation;
Sun, 03 Oct 1999 15:52:53 +0200 wenzelm export token_source;
Sun, 03 Oct 1999 15:51:38 +0200 wenzelm added Space, Comment token kinds (keep actual text);
Fri, 01 Oct 1999 20:41:58 +0200 wenzelm fixed no_qed;
Fri, 01 Oct 1999 20:40:03 +0200 wenzelm added Isar/obtain.ML;
Fri, 01 Oct 1999 20:39:40 +0200 wenzelm improved 'fix' / Skolem interfaces;
Fri, 01 Oct 1999 20:38:50 +0200 wenzelm added 'obtain' command;
Fri, 01 Oct 1999 20:38:16 +0200 wenzelm tuned comment;
Fri, 01 Oct 1999 20:38:00 +0200 wenzelm added prf_asm_goal;
Fri, 01 Oct 1999 20:37:38 +0200 wenzelm added atomic_thesis;
Fri, 01 Oct 1999 20:36:53 +0200 wenzelm The 'obtain' language element -- achieves (eliminated) existential
Fri, 01 Oct 1999 18:36:12 +0200 wenzelm added undef_global_attribute, undef_local_attribute;
Fri, 01 Oct 1999 10:23:13 +0200 berghofe - Fixed bug in mk_split_pack which caused application of expansion theorem
Thu, 30 Sep 1999 23:37:22 +0200 wenzelm fixed 'is' match;
Thu, 30 Sep 1999 23:33:41 +0200 wenzelm added cert_skolem;
Thu, 30 Sep 1999 23:31:55 +0200 wenzelm export find_free;
Thu, 30 Sep 1999 23:31:13 +0200 wenzelm removed ProofContext.declare_thm;
Thu, 30 Sep 1999 21:23:08 +0200 wenzelm local_def_i: typ option;
Thu, 30 Sep 1999 21:22:26 +0200 wenzelm fix_i, local_def_i: typ option;
Thu, 30 Sep 1999 21:21:52 +0200 wenzelm get_goal: prop;
Thu, 30 Sep 1999 21:21:04 +0200 wenzelm insert: ignore facts;
Thu, 30 Sep 1999 21:20:36 +0200 wenzelm export def_sort, def_type;
Thu, 30 Sep 1999 20:49:06 +0200 wenzelm Real/HahnBanach;
Thu, 30 Sep 1999 16:16:56 +0200 wenzelm depend on Main;
Thu, 30 Sep 1999 10:06:56 +0200 paulson now with (weak safety) guarantees (weak progress) with Extend
Wed, 29 Sep 1999 16:45:23 +0200 wenzelm bind_thm ("case_split", case_split_thm);
Wed, 29 Sep 1999 16:45:04 +0200 wenzelm CollectE;
Wed, 29 Sep 1999 16:44:18 +0200 wenzelm subsetD;
Wed, 29 Sep 1999 16:41:52 +0200 wenzelm update from Gertrud;
Wed, 29 Sep 1999 15:35:09 +0200 wenzelm The Hahn-Banach theorem for real vectorspaces;
Wed, 29 Sep 1999 14:56:49 +0200 wenzelm bind_thms;
Wed, 29 Sep 1999 14:56:19 +0200 wenzelm Sign.defaultS;
Wed, 29 Sep 1999 14:56:01 +0200 wenzelm Sign.of_sort;
Wed, 29 Sep 1999 14:40:15 +0200 wenzelm tuned;
Wed, 29 Sep 1999 14:40:07 +0200 wenzelm removed force_strip_shyps;
Wed, 29 Sep 1999 14:39:35 +0200 wenzelm lemma;
Wed, 29 Sep 1999 14:38:03 +0200 wenzelm bind_thms;
Wed, 29 Sep 1999 14:36:36 +0200 wenzelm proper handling of dangling sort hypotheses (at last!);
Wed, 29 Sep 1999 14:36:04 +0200 wenzelm mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
Wed, 29 Sep 1999 14:35:18 +0200 wenzelm Sign.defaultS;
Wed, 29 Sep 1999 14:34:01 +0200 wenzelm strip_shyps(_warning);
Wed, 29 Sep 1999 14:03:57 +0200 wenzelm mg_domain: exception DOMAIN;
Wed, 29 Sep 1999 14:02:33 +0200 wenzelm removed implies_intr_shyps;
Wed, 29 Sep 1999 13:55:58 +0200 wenzelm added witness_sorts, univ_witness;
Wed, 29 Sep 1999 13:54:31 +0200 wenzelm added witness_sorts, univ_witness;
Wed, 29 Sep 1999 13:52:01 +0200 wenzelm handle Sorts.DOMAIN;
Wed, 29 Sep 1999 13:51:41 +0200 wenzelm added rems_sort;
Wed, 29 Sep 1999 13:51:23 +0200 wenzelm use Drule.strip_shyps_warning;
Wed, 29 Sep 1999 13:50:48 +0200 wenzelm strip_shyps_warning;
Wed, 29 Sep 1999 13:50:26 +0200 wenzelm new tsig components;
Wed, 29 Sep 1999 13:49:49 +0200 wenzelm more sections;
Wed, 29 Sep 1999 13:49:27 +0200 wenzelm present sections;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip