wenzelm [Mon, 04 Oct 1999 21:39:10 +0200] rev 7695
mk_frees, assume_read moved here;
FOLogic.mk_conj, FOLogic.mk_disj;
wenzelm [Mon, 04 Oct 1999 21:37:35 +0200] rev 7694
tryres, gen_make_elim moved here;
wenzelm [Mon, 04 Oct 1999 21:37:00 +0200] rev 7693
FOLogic.mk_conj;
wenzelm [Mon, 04 Oct 1999 21:35:26 +0200] rev 7692
added mk_conj, mk_disj, mk_imp;
wenzelm [Mon, 04 Oct 1999 21:34:20 +0200] rev 7691
added BVC;
wenzelm [Mon, 04 Oct 1999 14:45:35 +0200] rev 7690
added mk_conj, mk_disj, mk_imp;
paulson [Mon, 04 Oct 1999 13:47:28 +0200] rev 7689
working snapshot (even Alloc)
paulson [Mon, 04 Oct 1999 13:45:31 +0200] rev 7688
most results now refer to those for "extend"
wenzelm [Mon, 04 Oct 1999 12:22:14 +0200] rev 7687
fixed lookup_theory;
paulson [Mon, 04 Oct 1999 10:19:18 +0200] rev 7686
fixed CHANGED_GOAL, which is used by stac
wenzelm [Sun, 03 Oct 1999 15:54:25 +0200] rev 7685
improved theory_source presentation (hook);
wenzelm [Sun, 03 Oct 1999 15:54:04 +0200] rev 7684
improved theory_source presentation;
wenzelm [Sun, 03 Oct 1999 15:52:53 +0200] rev 7683
export token_source;
improved Present.theory_source;
wenzelm [Sun, 03 Oct 1999 15:51:38 +0200] rev 7682
added Space, Comment token kinds (keep actual text);
source: do not filter proper;
wenzelm [Fri, 01 Oct 1999 20:41:58 +0200] rev 7681
fixed no_qed;
wenzelm [Fri, 01 Oct 1999 20:40:03 +0200] rev 7680
added Isar/obtain.ML;
wenzelm [Fri, 01 Oct 1999 20:39:40 +0200] rev 7679
improved 'fix' / Skolem interfaces;
wenzelm [Fri, 01 Oct 1999 20:38:50 +0200] rev 7678
added 'obtain' command;
wenzelm [Fri, 01 Oct 1999 20:38:16 +0200] rev 7677
tuned comment;
wenzelm [Fri, 01 Oct 1999 20:38:00 +0200] rev 7676
added prf_asm_goal;
wenzelm [Fri, 01 Oct 1999 20:37:38 +0200] rev 7675
added atomic_thesis;
wenzelm [Fri, 01 Oct 1999 20:36:53 +0200] rev 7674
The 'obtain' language element -- achieves (eliminated) existential
quantification proof command level.
wenzelm [Fri, 01 Oct 1999 18:36:12 +0200] rev 7673
added undef_global_attribute, undef_local_attribute;
berghofe [Fri, 01 Oct 1999 10:23:13 +0200] rev 7672
- Fixed bug in mk_split_pack which caused application of expansion theorem
to fail because of typing reasons
- Rewrote inst_lift and inst_split: now cterm_instantiate is used to
instantiate theorems
wenzelm [Thu, 30 Sep 1999 23:37:22 +0200] rev 7671
fixed 'is' match;
wenzelm [Thu, 30 Sep 1999 23:33:41 +0200] rev 7670
added cert_skolem;
removed declare_thm;
context: removed maxidx;
added maxidx_of_pair for proper unification;
wenzelm [Thu, 30 Sep 1999 23:31:55 +0200] rev 7669
export find_free;
wenzelm [Thu, 30 Sep 1999 23:31:13 +0200] rev 7668
removed ProofContext.declare_thm;
wenzelm [Thu, 30 Sep 1999 21:23:08 +0200] rev 7667
local_def_i: typ option;
admit additional (fixed) type vars on rhs;
wenzelm [Thu, 30 Sep 1999 21:22:26 +0200] rev 7666
fix_i, local_def_i: typ option;
wenzelm [Thu, 30 Sep 1999 21:21:52 +0200] rev 7665
get_goal: prop;
fix_i: typ option;
wenzelm [Thu, 30 Sep 1999 21:21:04 +0200] rev 7664
insert: ignore facts;
wenzelm [Thu, 30 Sep 1999 21:20:36 +0200] rev 7663
export def_sort, def_type;
fix_i: typ option;
init: maxidx = 0 is workaround for obscure bug in Unify.smash_unifiers;
wenzelm [Thu, 30 Sep 1999 20:49:06 +0200] rev 7662
Real/HahnBanach;
wenzelm [Thu, 30 Sep 1999 16:16:56 +0200] rev 7661
depend on Main;
paulson [Thu, 30 Sep 1999 10:06:56 +0200] rev 7660
now with (weak safety) guarantees (weak progress) with Extend
wenzelm [Wed, 29 Sep 1999 16:45:23 +0200] rev 7659
bind_thm ("case_split", case_split_thm);
wenzelm [Wed, 29 Sep 1999 16:45:04 +0200] rev 7658
CollectE;
AddXIs [subsetD, rev_subsetD, psubsetI];
wenzelm [Wed, 29 Sep 1999 16:44:18 +0200] rev 7657
subsetD;
wenzelm [Wed, 29 Sep 1999 16:41:52 +0200] rev 7656
update from Gertrud;
wenzelm [Wed, 29 Sep 1999 15:35:09 +0200] rev 7655
The Hahn-Banach theorem for real vectorspaces;
wenzelm [Wed, 29 Sep 1999 14:56:49 +0200] rev 7654
bind_thms;
wenzelm [Wed, 29 Sep 1999 14:56:19 +0200] rev 7653
Sign.defaultS;
wenzelm [Wed, 29 Sep 1999 14:56:01 +0200] rev 7652
Sign.of_sort;
wenzelm [Wed, 29 Sep 1999 14:40:15 +0200] rev 7651
tuned;
wenzelm [Wed, 29 Sep 1999 14:40:07 +0200] rev 7650
removed force_strip_shyps;
wenzelm [Wed, 29 Sep 1999 14:39:35 +0200] rev 7649
lemma;
wenzelm [Wed, 29 Sep 1999 14:38:03 +0200] rev 7648
bind_thms;
wenzelm [Wed, 29 Sep 1999 14:36:36 +0200] rev 7647
proper handling of dangling sort hypotheses (at last!);
wenzelm [Wed, 29 Sep 1999 14:36:04 +0200] rev 7646
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
(asm_simp performance!);
wenzelm [Wed, 29 Sep 1999 14:35:18 +0200] rev 7645
Sign.defaultS;
wenzelm [Wed, 29 Sep 1999 14:34:01 +0200] rev 7644
strip_shyps(_warning);
wenzelm [Wed, 29 Sep 1999 14:03:57 +0200] rev 7643
mg_domain: exception DOMAIN;
proper witness_sorts;
removed nonempty_sort;
wenzelm [Wed, 29 Sep 1999 14:02:33 +0200] rev 7642
removed implies_intr_shyps;
removed force_strip_shyps (at last!);
strip_shyps: proper witness_sorts;
fix_shyps: tuned for all_sorts_nonempty;
wenzelm [Wed, 29 Sep 1999 13:55:58 +0200] rev 7641
added witness_sorts, univ_witness;
removed nonempty_sort;
tsig: log_types, univ_witness (require rebuild_tsig!);
heavily tuned;
wenzelm [Wed, 29 Sep 1999 13:54:31 +0200] rev 7640
added witness_sorts, univ_witness;
removed nonempty_sort;
wenzelm [Wed, 29 Sep 1999 13:52:01 +0200] rev 7639
handle Sorts.DOMAIN;
wenzelm [Wed, 29 Sep 1999 13:51:41 +0200] rev 7638
added rems_sort;
wenzelm [Wed, 29 Sep 1999 13:51:23 +0200] rev 7637
use Drule.strip_shyps_warning;
removed Thm.implies_intr_shyps;
wenzelm [Wed, 29 Sep 1999 13:50:48 +0200] rev 7636
strip_shyps_warning;