Page MenuHomeIsabelle/Phabricator
Feed All Stories

Today

paulson <lp15@cam.ac.uk> committed rAFP9c345dca84b6: Fixed a use of Bochner_Integration.integrable_cong.
Fixed a use of Bochner_Integration.integrable_cong
Wed, May 25, 3:05 PM
paulson <lp15@cam.ac.uk> committed rAFP31801addfd8a: Tidying/removal of obsolete material.
Tidying/removal of obsolete material
Wed, May 25, 3:05 PM
paulson <lp15@cam.ac.uk> committed rAFPd54d7aa85968: fixes for compatibility with renamed / new lemmas.
fixes for compatibility with renamed / new lemmas
Wed, May 25, 12:01 PM
paulson <lp15@cam.ac.uk> committed rISABELLE8e2285baadba: qualified name to fix integrable_cong ambiguity.
qualified name to fix integrable_cong ambiguity
Wed, May 25, 11:58 AM
paulson <lp15@cam.ac.uk> committed rISABELLE7448423e5dba: Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted….
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted…
Wed, May 25, 11:58 AM

Mon, May 23

paulson <lp15@cam.ac.uk> committed rISABELLE4c3bc0d2568f: Eliminated two unnecessary inductions.
Eliminated two unnecessary inductions
Mon, May 23, 6:22 PM
paulson <lp15@cam.ac.uk> committed rAFP9831a6481d33: Tiny simplifications.
Tiny simplifications
Mon, May 23, 2:07 PM
desharna committed rISABELLEec4b514bcfad: added lemma image_mset_filter_mset_swap.
added lemma image_mset_filter_mset_swap
Mon, May 23, 1:56 PM
desharna committed rISABELLE7c2fe41f5ee8: NEWS.
NEWS
Mon, May 23, 1:56 PM
desharna committed rISABELLE4117491aa7fe: merged.
merged
Mon, May 23, 10:13 AM
desharna committed rISABELLEcbf011677235: added lemmas filter_mset_cong{0,}.
added lemmas filter_mset_cong{0,}
Mon, May 23, 10:13 AM

Sun, May 22

florian.haftmann committed rISABELLE160c9c18a707: »nil« seems to be a reserved constructor word in PolyML.
»nil« seems to be a reserved constructor word in PolyML
Sun, May 22, 8:02 AM

Wed, May 18

paulson <lp15@cam.ac.uk> committed rAFPd859db6acb75: A tiny bit of reorganisation.
A tiny bit of reorganisation
Wed, May 18, 5:18 PM
paulson <lp15@cam.ac.uk> committed rISABELLE91c16c5ad3e9: tidied auto / simp with null arguments.
tidied auto / simp with null arguments
Wed, May 18, 11:51 AM

Tue, May 17

paulson <lp15@cam.ac.uk> committed rAFP3149eae9c077: the last "simp/auto" problems.
the last "simp/auto" problems
Tue, May 17, 5:03 PM
paulson <lp15@cam.ac.uk> committed rAFP58359778acff: corrected all "bysimp".
corrected all "bysimp"
Tue, May 17, 4:34 PM
paulson <lp15@cam.ac.uk> committed rAFP1668bf4eba40: Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/So….
Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/So…
Tue, May 17, 3:25 PM
paulson <lp15@cam.ac.uk> committed rAFPef2cf009504d: Tidied auto/simp with null arguments.
Tidied auto/simp with null arguments
Tue, May 17, 3:25 PM
nipkow committed rAFP173359fcafa4: merged.
merged
Tue, May 17, 7:45 AM
nipkow committed rAFP3ec6dc59412e: comleted single loop refinement.
comleted single loop refinement
Tue, May 17, 7:45 AM

Mon, May 16

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP613d8d8fb067: minor adjustments.
minor adjustments
Mon, May 16, 11:36 AM
user9716869 <user9716869@gmail.com> committed rAFPda39b5964de3: metadata.
metadata
Mon, May 16, 2:26 AM
user9716869 <user9716869@gmail.com> committed rAFPb4f4acb4ee94: minor amendments.
minor amendments
Mon, May 16, 1:15 AM
user9716869 <user9716869@gmail.com> committed rAFP68412a363595: creation and preservation of limits; a variety of auxiliary results and….
creation and preservation of limits; a variety of auxiliary results and…
Mon, May 16, 1:09 AM

Fri, May 13

Fabian Huch <huch@in.tum.de> committed rAFPd0c948a42af2: merged.
merged
Fri, May 13, 5:01 PM
Fabian Huch <huch@in.tum.de> committed rAFP00c034528a4a: clarified formatting, for the sake of scala3;.
clarified formatting, for the sake of scala3;
Fri, May 13, 5:01 PM
Fabian Huch <huch@in.tum.de> committed rAFPdbddab778577: merged.
merged
Fri, May 13, 5:01 PM
Fabian Huch <huch@in.tum.de> committed rAFPe3c2aeafc2c0: merged.
merged
Fri, May 13, 5:01 PM
Fabian Huch <huch@in.tum.de> committed rAFPfbafb44dc503: hugo site: better scrolling;.
hugo site: better scrolling;
Fri, May 13, 5:01 PM

Thu, May 12

paulson <lp15@cam.ac.uk> committed rAFPa3f22844a82d: patched a broken proof.
patched a broken proof
Thu, May 12, 12:19 PM
nipkow committed rAFP198ec6433df8: merged.
merged
Thu, May 12, 11:58 AM
nipkow committed rAFP8bcb5f82bf5b: single lopp variant refined to lists..
single lopp variant refined to lists.
Thu, May 12, 11:58 AM

Wed, May 11

makarius committed rISABELLE295e1c9d2994: tuned signature;.
tuned signature;
Wed, May 11, 10:43 AM
makarius committed rISABELLEe2aa3c1f90a1: provide Isabelle/Electron test;.
provide Isabelle/Electron test;
Wed, May 11, 10:13 AM

Tue, May 10

kleing committed rAFPfd202ff69233: merge from afp-2021-1.
merge from afp-2021-1
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFPd7801c6a5adf: sitegen for Digit_Expansions.
sitegen for Digit_Expansions
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFP5e69ff8cfad7: typo fix.
typo fix
Tue, May 10, 1:25 AM
kleing committed rAFP9a8e97891573: adjust for isabelle@7095df141819.
adjust for isabelle@7095df141819
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFP143b4d24fbba: New entry Digit_Expansions.
New entry Digit_Expansions
Tue, May 10, 1:25 AM
paulson committed rAFP1f559dbb866d: merged.
merged
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFPb11ab6e691fc: finally!!!! Sitegen for Sophomore's Dream.
finally!!!! Sitegen for Sophomore's Dream
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFP374cb39d1be9: Updating the version of Jinja2, as suggested by Manuel.
Updating the version of Jinja2, as suggested by Manuel
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFP29dee38f86fa: Minor corrections to metadata (no "and" between authors' names).
Minor corrections to metadata (no "and" between authors' names)
Tue, May 10, 1:25 AM
paulson committed rAFPcccf7f8d03c4: merged.
merged
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFPee785c9dce1a: new entry Sophomores_Dream.
new entry Sophomores_Dream
Tue, May 10, 1:25 AM
paulson <lp15@cam.ac.uk> committed rAFPbf87ecbb9af7: updated metadata.
updated metadata
Tue, May 10, 1:25 AM
pruvisto committed rAFPb8c4aec14ebf: updated name and email address of Rose Bohrer.
updated name and email address of Rose Bohrer
Tue, May 10, 1:24 AM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP75635e4f695b: new entry Clique_and_Monotone_Circuits.
new entry Clique_and_Monotone_Circuits
Tue, May 10, 1:24 AM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP05cff0f17aaf: sitegen for Clique_and_Monotone_Circuits.
sitegen for Clique_and_Monotone_Circuits
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1da45ba16d3e: new entry: Fisher's Inequality.
new entry: Fisher's Inequality
Tue, May 10, 1:24 AM
nipkow committed rAFP7c00f83aacff: New entry Multiset_Ordering_NPC.
New entry Multiset_Ordering_NPC
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa6a2db6744be: metadata and sitegen for Fisher's inequality.
metadata and sitegen for Fisher's inequality
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP11b4b5caf3fe: metadata and sitegen for Prefix_Free_Code_Combinators.
metadata and sitegen for Prefix_Free_Code_Combinators
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa108597c1ee8: new entry: Frequence_Moments.
new entry: Frequence_Moments
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP0f61fdaf00bf: sitegen for Frequence_Moments.
sitegen for Frequence_Moments
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP4895a13e16de: new entry: Prefix_Free_Code_Combinators.
new entry: Prefix_Free_Code_Combinators
Tue, May 10, 1:24 AM
kleing committed rAFPa6affb2d1770: regen website (some orders are different in python3).
regen website (some orders are different in python3)
Tue, May 10, 1:24 AM
kleing committed rAFPcac9b963c170: switch sitegen to python3.
switch sitegen to python3
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1de107e93d5c: sitegen for new entry.
sitegen for new entry
Tue, May 10, 1:24 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP06b9a0364651: new entry: FOL_Seq_Calc3.
new entry: FOL_Seq_Calc3
Tue, May 10, 1:24 AM
nipkow committed rAFPe1c3276c598b: New entry: Dedekind_Real.
New entry: Dedekind_Real
Tue, May 10, 1:24 AM
paulson <lp15@cam.ac.uk> committed rAFP74cbc440d11b: Cotangent_PFD_Formula sitegen.
Cotangent_PFD_Formula sitegen
Tue, May 10, 1:24 AM
nipkow committed rAFPc296f652adc9: New entry Ackermann_not_PR, from distribution.
New entry Ackermann_not_PR, from distribution
Tue, May 10, 1:24 AM
paulson <lp15@cam.ac.uk> committed rAFPe08bf2dbf0e3: new entry Cotangent_PFD_Formula.
new entry Cotangent_PFD_Formula
Tue, May 10, 1:24 AM
paulson <lp15@cam.ac.uk> committed rAFPa304d5d49542: website for Independence_CH.
website for Independence_CH
Tue, May 10, 1:24 AM
paulson <lp15@cam.ac.uk> committed rAFPf0c701e6661f: new entry Independence_CH.
new entry Independence_CH
Tue, May 10, 1:24 AM
nipkow committed rAFPbf120ce6a2ff: New entry ResiduatedTransitionSystem.
New entry ResiduatedTransitionSystem
Tue, May 10, 1:24 AM
paulson <lp15@cam.ac.uk> committed rAFPdeb6c18fa953: Transitive_Models webpage.
Transitive_Models webpage
Tue, May 10, 1:24 AM
paulson <lp15@cam.ac.uk> committed rAFP6ed8e38ee242: new entry Transitive_Models.
new entry Transitive_Models
Tue, May 10, 1:24 AM

Mon, May 9

makarius committed rISABELLE7095df141819: tuned text;.
tuned text;
Mon, May 9, 9:01 PM
pruvisto committed rAFP4ef570cafca9: updated name and email address of Rose Bohrer.
updated name and email address of Rose Bohrer
Mon, May 9, 3:38 PM
makarius committed rISABELLE5acc4de7db89: tuned text;.
tuned text;
Mon, May 9, 1:41 PM

Fri, May 6

paulson <lp15@cam.ac.uk> committed rISABELLEf16d83de3e4a: Tidied up some super-messy proofs.
Tidied up some super-messy proofs
Fri, May 6, 6:04 PM
paulson <lp15@cam.ac.uk> committed rAFP6ae899d8db32: Removal of unnecessary material.
Removal of unnecessary material
Fri, May 6, 11:50 AM
paulson <lp15@cam.ac.uk> committed rISABELLE51e05af57455: Added a couple of obvious simprules.
Added a couple of obvious simprules
Fri, May 6, 11:42 AM

Wed, May 4

nipkow committed rISABELLE53a60eae475f: added lemma.
added lemma
Wed, May 4, 7:47 AM

Mon, May 2

paulson <lp15@cam.ac.uk> committed rAFP0915660e2387: perfectly pointless streamlining.
perfectly pointless streamlining
Mon, May 2, 11:53 AM

Sat, Apr 30

paulson <lp15@cam.ac.uk> committed rAFP33748b892d11: More general definition of gcard.
More general definition of gcard
Sat, Apr 30, 8:50 PM

Tue, Apr 26

dcjm committed rPOLYML50ce3dd5a5f9: Fix segfault as a result of a call to INet6Sock.any. It was calling the IPv4… (authored by dcjm).
Fix segfault as a result of a call to INet6Sock.any. It was calling the IPv4…
Tue, Apr 26, 9:50 PM
dcjm committed rPOLYMLbafe319bc3a6: Remove reference to "make compiler" from instructions. This is no longer… (authored by dcjm).
Remove reference to "make compiler" from instructions. This is no longer…
Tue, Apr 26, 9:50 PM
makarius committed rISABELLEd1417d9c6deb: tuned signature: avoid problems with scala3;.
tuned signature: avoid problems with scala3;
Tue, Apr 26, 11:16 AM
makarius committed rISABELLE691ed9f41729: proper indentation;.
proper indentation;
Tue, Apr 26, 11:16 AM

Mon, Apr 25

nipkow committed rAFP15a6b7cce9c7: refined one-loop version further.
refined one-loop version further
Mon, Apr 25, 3:22 PM

Apr 22 2022

makarius committed rISABELLE331f96a67924: clarified management of interpreter threads: more generic;.
clarified management of interpreter threads: more generic;
Apr 22 2022, 10:59 AM
makarius committed rISABELLEdf9d869cd5fd: merged.
merged
Apr 22 2022, 10:59 AM
makarius committed rISABELLEd6f2fbdc6322: clarified signature;.
clarified signature;
Apr 22 2022, 10:59 AM
makarius committed rISABELLE39011d0d2128: tuned signature;.
tuned signature;
Apr 22 2022, 10:59 AM
makarius committed rISABELLEd5041b68a237: clarified signature;.
clarified signature;
Apr 22 2022, 10:59 AM
makarius committed rISABELLE400e325a5416: clarified signature, based on hints by IntelliJ IDEA;.
clarified signature, based on hints by IntelliJ IDEA;
Apr 22 2022, 10:59 AM
makarius committed rISABELLEe1c9e4d59921: more robust: avoid partiality;.
more robust: avoid partiality;
Apr 22 2022, 10:59 AM
makarius committed rISABELLE96293bd077bb: tuned;.
tuned;
Apr 22 2022, 10:59 AM
makarius committed rISABELLE40630fec3b5d: clarified signature;.
clarified signature;
Apr 22 2022, 10:59 AM
makarius committed rISABELLE7b417c578b19: clarified signature;.
clarified signature;
Apr 22 2022, 10:59 AM
makarius committed rISABELLEc8087e6bd2ce: tuned --- avoid warnings in scala3;.
tuned --- avoid warnings in scala3;
Apr 22 2022, 10:59 AM
makarius committed rISABELLEf6ee58333aa5: clarified signature;.
clarified signature;
Apr 22 2022, 10:59 AM

Apr 18 2022

paulson <lp15@cam.ac.uk> committed rAFPb2708c764337: tidied up a few proofs.
tidied up a few proofs
Apr 18 2022, 10:44 PM

Apr 13 2022

paulson <lp15@cam.ac.uk> committed rAFPc74a55e029d0: A bit of beautification.
A bit of beautification
Apr 13 2022, 5:57 PM
blanchette committed rISABELLEa36a1cc0144c: pass new option only to new version of E.
pass new option only to new version of E
Apr 13 2022, 4:58 PM

Apr 12 2022

paulson <lp15@cam.ac.uk> committed rAFPa2db1b041475: Yet more tidying and streamlining of graph lemmas.
Yet more tidying and streamlining of graph lemmas
Apr 12 2022, 1:41 PM

Apr 11 2022

desharna committed rISABELLE6b38054241b8: merged.
merged
Apr 11 2022, 2:06 PM