Page MenuHomeIsabelle/Phabricator

Open Tasks

Low (6)

Wishlist (1)

Active Repositories

Recent Activity

Yesterday

paulson <lp15@cam.ac.uk> committed rISABELLE67d87d224e00: A few new lemmas plus some refinements.
A few new lemmas plus some refinements
Fri, Oct 15, 4:44 PM
paulson <lp15@cam.ac.uk> committed rAFP70694297a67c: Simplified a definition.
Simplified a definition
Fri, Oct 15, 4:31 PM
nanjiang <nanjiang@whu.edu.cn> committed rAFP96920cdaac55: modify propa.
modify propa
Fri, Oct 15, 3:44 PM

Thu, Oct 14

desharna committed rISABELLEc434f4e74947: merged.
merged
Thu, Oct 14, 3:27 PM
desharna committed rISABELLE6d111935299c: produced Mirabelle output directly in ML until Scala output gets fixed.
produced Mirabelle output directly in ML until Scala output gets fixed
Thu, Oct 14, 3:27 PM
florian.haftmann committed rAFPb29e73d246d4: bit singleton shifts recovered for the sake of backward compatibility.
bit singleton shifts recovered for the sake of backward compatibility
Thu, Oct 14, 9:54 AM
kleing committed rAFP323c29c97a1e: close merged branch.
close merged branch
Thu, Oct 14, 1:25 AM

Wed, Oct 13

makarius committed rISABELLEf24ade4ff3cc: clarified signature;.
clarified signature;
Wed, Oct 13, 4:53 PM
makarius committed rISABELLE21a20b990724: clarified signature;.
clarified signature;
Wed, Oct 13, 4:53 PM
makarius committed rISABELLE3315c551fe6e: clarified signature;.
clarified signature;
Wed, Oct 13, 4:53 PM
makarius committed rISABELLEa241eadc0e3f: removed unused material (left-over from fd0c85d7da38);.
removed unused material (left-over from fd0c85d7da38);
Wed, Oct 13, 4:53 PM
makarius committed rISABELLEd97c48dc87fa: support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);.
support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);
Wed, Oct 13, 12:08 AM
makarius committed rISABELLEce8152fb021b: removed junk;.
removed junk;
Wed, Oct 13, 12:08 AM

Tue, Oct 12

nipkow committed rAFP8d2f2c35b69d: updated to 7422950f3955.
updated to 7422950f3955
Tue, Oct 12, 8:59 PM
nipkow committed rISABELLE403ce50e6a2a: separated commands from annotations to be able to abstract about the latter only.
separated commands from annotations to be able to abstract about the latter only
Tue, Oct 12, 8:58 PM
nipkow committed rISABELLE7422950f3955: merged.
merged
Tue, Oct 12, 8:58 PM
makarius committed rISABELLE0803dd7f920d: tuned comments;.
tuned comments;
Tue, Oct 12, 7:22 PM
makarius committed rISABELLE907483081d4c: prefer standard Term.dest_abs, with minor deviation of generated names;.
prefer standard Term.dest_abs, with minor deviation of generated names;
Tue, Oct 12, 7:22 PM
Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFP7a7acbc421da: merge.
merge
Tue, Oct 12, 5:03 PM
Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFP8fda5e92692f: EPO: simplify proof.
EPO: simplify proof
Tue, Oct 12, 5:03 PM

Mon, Oct 11

nipkow committed rISABELLE40f03761f77f: more examples.
more examples
Mon, Oct 11, 9:55 PM
florian.haftmann committed rAFP134b70fc858e: primer.
primer
Mon, Oct 11, 9:41 PM
dcjm committed rPOLYMLc3c107f844b9: Fix passing structures of size 8-16 bytes in SysV X86/64. Fixes #162. (authored by dcjm).
Fix passing structures of size 8-16 bytes in SysV X86/64. Fixes #162.
Mon, Oct 11, 7:13 PM
makarius committed rISABELLE059743bc8311: workaround for old macOS versions, after change of Let's Encrypt root….
workaround for old macOS versions, after change of Let's Encrypt root…
Mon, Oct 11, 5:06 PM
florian.haftmann committed rISABELLE27475e64a887: more complete simp rules.
more complete simp rules
Mon, Oct 11, 1:26 PM
florian.haftmann committed rAFPf8dc7663c3cf: more complete simp rules.
more complete simp rules
Mon, Oct 11, 1:25 PM
florian.haftmann committed rAFP052886ce16c0: more complete simp rules (examples).
more complete simp rules (examples)
Mon, Oct 11, 8:33 AM
florian.haftmann committed rISABELLE9c04a82c3128: more complete simp rules.
more complete simp rules
Mon, Oct 11, 8:32 AM

Sun, Oct 10

florian.haftmann committed rISABELLE807b094a9b78: avoid overaggressive contraction of conversions.
avoid overaggressive contraction of conversions
Sun, Oct 10, 5:46 PM
florian.haftmann committed rAFPc42c2c2447c2: avoid overaggressive contraction of conversions.
avoid overaggressive contraction of conversions
Sun, Oct 10, 5:45 PM
florian.haftmann committed rAFP721d0f625e02: slightly more prominence for proof tools; more examples.
slightly more prominence for proof tools; more examples
Sun, Oct 10, 8:02 AM
florian.haftmann committed rISABELLEbc27c490aaac: normalizing NOT (numeral _) (again).
normalizing NOT (numeral _) (again)
Sun, Oct 10, 8:01 AM

Fri, Oct 8

makarius created Blog Post: Nitpick with external/portable MiniSat.
Fri, Oct 8, 11:25 AM
makarius committed rISABELLEe593ea880494: tuned text;.
tuned text;
Fri, Oct 8, 10:57 AM
user9716869 <user9716869@gmail.com> committed rAFP7ecd220edef3: ETTS: minor amendments.
ETTS: minor amendments
Fri, Oct 8, 1:12 AM

Thu, Oct 7

makarius committed rISABELLEf4c5e8ca1d53: recover NEWS from 78d1f73bbeaa;.
recover NEWS from 78d1f73bbeaa;
Thu, Oct 7, 11:42 PM
makarius committed rISABELLE59ef23ac81ab: save 90 MB by excluding rlwrap and thus perl;.
save 90 MB by excluding rlwrap and thus perl;
Thu, Oct 7, 11:42 PM
makarius committed rISABELLE122615955fc0: save 45 MB by excluding rlwrap and thus perl;.
save 45 MB by excluding rlwrap and thus perl;
Thu, Oct 7, 11:26 PM
user9716869 <user9716869@gmail.com> committed rAFP28ce3268cde2: CTR and ETTS: integration with fd5f62176987.
CTR and ETTS: integration with fd5f62176987
Thu, Oct 7, 11:02 PM
makarius committed rISABELLEdd18b59aded7: NEWS;.
NEWS;
Thu, Oct 7, 10:59 PM