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

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
Restructured lin.arith.package and fixed a proof in RComplete.
1999-09-23, by nipkow
Restructured lin.arith.package.
1999-09-23, by nipkow
thms_containing: single writeln;
1999-09-22, by wenzelm
tuned pretty_thms;
1999-09-22, by wenzelm
added thms_containing;
1999-09-22, by wenzelm
qed "";
1999-09-22, by wenzelm
proper theory setup for Real/ex/BinEx;
1999-09-22, by wenzelm
tuned;
1999-09-22, by wenzelm

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

isabelle