isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

proper dependencies of all theories and packages;
1999-10-04, by wenzelm
removed DatatypePackage.setup;
1999-10-04, by wenzelm
load / setup recdef package (TFL);
1999-10-04, by wenzelm
load / setup datatype package;
1999-10-04, by wenzelm
removed TFL/sys.sml;
1999-10-04, by wenzelm
obsolete;
1999-10-04, by wenzelm
renamed 'prefix' to 'prfx' (avoids clash with infix);
1999-10-04, by wenzelm
tuned;
1999-10-04, by wenzelm
mk_frees, assume_read moved here;
1999-10-04, by wenzelm
tryres, gen_make_elim moved here;
1999-10-04, by wenzelm
FOLogic.mk_conj;
1999-10-04, by wenzelm
added mk_conj, mk_disj, mk_imp;
1999-10-04, by wenzelm
added BVC;
1999-10-04, by wenzelm
added mk_conj, mk_disj, mk_imp;
1999-10-04, by wenzelm
working snapshot (even Alloc)
1999-10-04, by paulson
most results now refer to those for "extend"
1999-10-04, by paulson
fixed lookup_theory;
1999-10-04, by wenzelm
fixed CHANGED_GOAL, which is used by stac
1999-10-04, by paulson
improved theory_source presentation (hook);
1999-10-03, by wenzelm
improved theory_source presentation;
1999-10-03, by wenzelm
export token_source;
1999-10-03, by wenzelm
added Space, Comment token kinds (keep actual text);
1999-10-03, by wenzelm
fixed no_qed;
1999-10-01, by wenzelm
added Isar/obtain.ML;
1999-10-01, by wenzelm
improved 'fix' / Skolem interfaces;
1999-10-01, by wenzelm
added 'obtain' command;
1999-10-01, by wenzelm
tuned comment;
1999-10-01, by wenzelm
added prf_asm_goal;
1999-10-01, by wenzelm
added atomic_thesis;
1999-10-01, by wenzelm
The 'obtain' language element -- achieves (eliminated) existential
1999-10-01, by wenzelm
added undef_global_attribute, undef_local_attribute;
1999-10-01, by wenzelm
- Fixed bug in mk_split_pack which caused application of expansion theorem
1999-10-01, by berghofe
fixed 'is' match;
1999-09-30, by wenzelm
added cert_skolem;
1999-09-30, by wenzelm
export find_free;
1999-09-30, by wenzelm
removed ProofContext.declare_thm;
1999-09-30, by wenzelm
local_def_i: typ option;
1999-09-30, by wenzelm
fix_i, local_def_i: typ option;
1999-09-30, by wenzelm
get_goal: prop;
1999-09-30, by wenzelm
insert: ignore facts;
1999-09-30, by wenzelm
export def_sort, def_type;
1999-09-30, by wenzelm
Real/HahnBanach;
1999-09-30, by wenzelm
depend on Main;
1999-09-30, by wenzelm
now with (weak safety) guarantees (weak progress) with Extend
1999-09-30, by paulson
bind_thm ("case_split", case_split_thm);
1999-09-29, by wenzelm
CollectE;
1999-09-29, by wenzelm
subsetD;
1999-09-29, by wenzelm
update from Gertrud;
1999-09-29, by wenzelm
The Hahn-Banach theorem for real vectorspaces;
1999-09-29, by wenzelm
bind_thms;
1999-09-29, by wenzelm
Sign.defaultS;
1999-09-29, by wenzelm
Sign.of_sort;
1999-09-29, by wenzelm
tuned;
1999-09-29, by wenzelm
removed force_strip_shyps;
1999-09-29, by wenzelm
lemma;
1999-09-29, by wenzelm
bind_thms;
1999-09-29, by wenzelm
proper handling of dangling sort hypotheses (at last!);
1999-09-29, by wenzelm
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
1999-09-29, by wenzelm
Sign.defaultS;
1999-09-29, by wenzelm
strip_shyps(_warning);
1999-09-29, by wenzelm
mg_domain: exception DOMAIN;
1999-09-29, by wenzelm
removed implies_intr_shyps;
1999-09-29, by wenzelm
added witness_sorts, univ_witness;
1999-09-29, by wenzelm
added witness_sorts, univ_witness;
1999-09-29, by wenzelm
handle Sorts.DOMAIN;
1999-09-29, by wenzelm
added rems_sort;
1999-09-29, by wenzelm
use Drule.strip_shyps_warning;
1999-09-29, by wenzelm
strip_shyps_warning;
1999-09-29, by wenzelm
new tsig components;
1999-09-29, by wenzelm
more sections;
1999-09-29, by wenzelm
present sections;
1999-09-29, by wenzelm
removed extra shyps error;
1999-09-29, by wenzelm
added string_of: text -> string;
1999-09-29, by wenzelm
working snapshot with new theory "Project"
1999-09-29, by paulson
tuned;
1999-09-28, by wenzelm
tidied, using "warning" function and fixing the Close_locale bug
1999-09-28, by paulson
added BCV.
1999-09-28, by nipkow
A new theory: a model of bytecode verification.
1999-09-28, by nipkow
zero_is_mult, by symmetry
1999-09-28, by paulson
new UNITY theory: Project
1999-09-28, by paulson
AC rules for equality
1999-09-28, by paulson
zero_is_mult, by symmetry
1999-09-28, by paulson
added W_correct -- correctness of Milner's type inference algorithm W
1999-09-28, by wenzelm
documented type solver
1999-09-28, by nipkow
incompatibility solver
1999-09-28, by nipkow
more tidying
1999-09-28, by paulson
removed order-sorted theorems from the default claset
1999-09-27, by paulson
added 'thms_containing', 'ML_setup';
1999-09-26, by wenzelm
added print_thms_containing;
1999-09-26, by wenzelm
use_mltext: Context.setmp only;
1999-09-26, by wenzelm
help: unknown theory context;
1999-09-26, by wenzelm
added keep', theory';
1999-09-26, by wenzelm
help: unkown theory context;
1999-09-26, by wenzelm
ThmDatabase.print_thms_containing;
1999-09-26, by wenzelm
added print_thms_containing;
1999-09-26, by wenzelm
defs: axmdecl;
1999-09-25, by wenzelm
simplified sectioned_args;
1999-09-25, by wenzelm
added reset_thms;
1999-09-25, by wenzelm
added reset_thms;
1999-09-25, by wenzelm
tuned;
1999-09-25, by wenzelm
defs: name mandatory;
1999-09-25, by wenzelm
avoid interrupts of read loop;
1999-09-25, by wenzelm
simplified sectioned_args;
1999-09-25, by wenzelm
Proof.reset_thms calculationN;
1999-09-25, by wenzelm
admit unbinding;
1999-09-25, by wenzelm
unfold / fold defs;
1999-09-25, by wenzelm
skolem_tag;
1999-09-25, by wenzelm
added fold_rule;
1999-09-25, by wenzelm
* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
1999-09-24, by wenzelm
working version with co-guarantees-leadsto results
1999-09-24, by paulson
tuned;
1999-09-24, by wenzelm
tuned;
1999-09-24, by wenzelm
qed "";
1999-09-24, by wenzelm
tuned print_result;
1999-09-23, by wenzelm
improved cycle error;
1999-09-23, by wenzelm
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
1999-09-23, by paulson
sep1 -> sep
1999-09-23, by nipkow
The restrict_to_left rule fixes some bugs
1999-09-23, by paulson
Sets new component "restrict_to_left"
1999-09-23, by paulson
tidied; added lemma restrict_to_left
1999-09-23, by paulson