Open Tasks
Open Tasks
Normal (6)
Normal (6)
- Nov 27 2021, 3:30 PM
Low (5)
Low (5)
Wishlist (4)
Wishlist (4)
Active Repositories
Active Repositories
- rAFP afp-devel
- Wed, Apr 17, 3:58 PM2024-04-17 15:58:42 (UTC+2)
- Mercurial
Recent Activity
Recent Activity
Today
Today
desharna committed rAFPd8aa8cc91178: added equivalence of concepts between First_Order_Terms.Position and HOL….
added equivalence of concepts between First_Order_Terms.Position and HOL…
Yesterday
Yesterday
update to jdk-21.0.3;
paulson <lp15@cam.ac.uk> committed rISABELLE601ff5c7cad5: Tidied up horrible archaic proofs.
Tidied up horrible archaic proofs
clarified signature;
make adhoc_overloading respect type constraints
desharna committed rAFP900cfb1adad1: added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp].
added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp]
Tue, Apr 16
Tue, Apr 16
clarified signature;
minor performance tuning: avoid redundant server access;
clarified modules and options (from store);
clarified signature;
clarified signature;
makarius committed rISABELLEc729b1d58982: more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);.
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
makarius committed rISABELLEdbcd6dc7f70f: back to static numa_nodes (reverting part of c2c59de57df9);.
back to static numa_nodes (reverting part of c2c59de57df9);
canonical time function for List.nth
Mon, Apr 15
Mon, Apr 15
paulson <lp15@cam.ac.uk> committed rISABELLE2fa018321400: Streamlining of many more archaic proofs.
Streamlining of many more archaic proofs
Fabian Huch <huch@in.tum.de> committed rISABELLE138b5172c7f8: clarified web app parameters: more flexible, using HTML5 id specification….
clarified web app parameters: more flexible, using HTML5 id specification…
Fabian Huch <huch@in.tum.de> committed rAFP7f16aa37c534: proper getopts;.
proper getopts;
Fabian Huch <huch@in.tum.de> committed rAFP5b2e7d535aff: tuned: use explicit keys;.
tuned: use explicit keys;
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFP408a29902df3: Removed inactive DOI.
Removed inactive DOI
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFPe0dfdf1b8ed4: Removed inactive DOI.
Removed inactive DOI
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd81723aa95cb: added monotonicity lemmas of lex/mul-ext.
added monotonicity lemmas of lex/mul-ext
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd8fb49658d5f: more showl-real instantiation to Show_Real thy.
more showl-real instantiation to Show_Real thy