berghofe [Tue, 05 Oct 1999 15:31:42 +0200] rev 7721
Tuned inductive definition.
wenzelm [Tue, 05 Oct 1999 15:31:39 +0200] rev 7720
updated;
wenzelm [Tue, 05 Oct 1999 15:30:58 +0200] rev 7719
added Thy/latex.ML;
removed Thy/browser_info.ML (stuff now in Thy/present.ML);
wenzelm [Tue, 05 Oct 1999 15:30:14 +0200] rev 7718
Present.setup;
berghofe [Tue, 05 Oct 1999 15:29:46 +0200] rev 7717
Added attribute rulify_prems (useful for modifying premises of introduction
rules of inductive sets).
wenzelm [Tue, 05 Oct 1999 15:29:36 +0200] rev 7716
added copy_all;
removed source;
wenzelm [Tue, 05 Oct 1999 15:28:37 +0200] rev 7715
clear: int arg;
wenzelm [Tue, 05 Oct 1999 15:26:10 +0200] rev 7714
added position;
berghofe [Tue, 05 Oct 1999 15:25:52 +0200] rev 7713
Additional rules for inductive package.
wenzelm [Tue, 05 Oct 1999 15:25:35 +0200] rev 7712
added untabify;
berghofe [Tue, 05 Oct 1999 15:24:58 +0200] rev 7711
Rule not_not is now stored in theory (needed by Inductive).
berghofe [Tue, 05 Oct 1999 15:23:22 +0200] rev 7710
Monotonicity rules for inductive definitions can now be added to a theory via
attribute "mono".
wenzelm [Tue, 05 Oct 1999 14:11:34 +0200] rev 7709
macros for Isabelle generated LaTeX output;
wenzelm [Mon, 04 Oct 1999 21:48:59 +0200] rev 7708
arithmetic now in IntArith;
wenzelm [Mon, 04 Oct 1999 21:48:23 +0200] rev 7707
simprocs now in IntArith;
wenzelm [Mon, 04 Oct 1999 21:47:16 +0200] rev 7706
IntArith;
wenzelm [Mon, 04 Oct 1999 21:46:49 +0200] rev 7705
Tools/typedef_package.ML;
wenzelm [Mon, 04 Oct 1999 21:46:13 +0200] rev 7704
eliminated ap/app;
wenzelm [Mon, 04 Oct 1999 21:45:10 +0200] rev 7703
proper dependencies of all theories and packages;
wenzelm [Mon, 04 Oct 1999 21:44:28 +0200] rev 7702
removed DatatypePackage.setup;
wenzelm [Mon, 04 Oct 1999 21:44:07 +0200] rev 7701
load / setup recdef package (TFL);
wenzelm [Mon, 04 Oct 1999 21:43:45 +0200] rev 7700
load / setup datatype package;
wenzelm [Mon, 04 Oct 1999 21:43:05 +0200] rev 7699
removed TFL/sys.sml;
removed Integ/simproc.ML, Integ/bin_simprocs.ML;
added Integ/IntArith.ML, Integ/IntArith.thy;
wenzelm [Mon, 04 Oct 1999 21:41:19 +0200] rev 7698
obsolete;
wenzelm [Mon, 04 Oct 1999 21:41:09 +0200] rev 7697
renamed 'prefix' to 'prfx' (avoids clash with infix);
wenzelm [Mon, 04 Oct 1999 21:39:36 +0200] rev 7696
tuned;
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;