isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

less more | (0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle