- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
May 25 2022
May 25 2022
paulson <lp15@cam.ac.uk> committed rAFP9c345dca84b6: Fixed a use of Bochner_Integration.integrable_cong.
Fixed a use of Bochner_Integration.integrable_cong
paulson <lp15@cam.ac.uk> committed rAFP31801addfd8a: Tidying/removal of obsolete material.
Tidying/removal of obsolete material
paulson <lp15@cam.ac.uk> committed rAFPd54d7aa85968: fixes for compatibility with renamed / new lemmas.
fixes for compatibility with renamed / new lemmas
paulson <lp15@cam.ac.uk> committed rISABELLE8e2285baadba: qualified name to fix integrable_cong ambiguity.
qualified name to fix integrable_cong ambiguity
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…
May 23 2022
May 23 2022
paulson <lp15@cam.ac.uk> committed rISABELLE4c3bc0d2568f: Eliminated two unnecessary inductions.
Eliminated two unnecessary inductions
paulson <lp15@cam.ac.uk> committed rAFP9831a6481d33: Tiny simplifications.
Tiny simplifications
desharna committed rISABELLEec4b514bcfad: added lemma image_mset_filter_mset_swap.
added lemma image_mset_filter_mset_swap
desharna committed rISABELLEcbf011677235: added lemmas filter_mset_cong{0,}.
added lemmas filter_mset_cong{0,}
May 22 2022
May 22 2022
florian.haftmann committed rISABELLE160c9c18a707: »nil« seems to be a reserved constructor word in PolyML.
»nil« seems to be a reserved constructor word in PolyML
May 18 2022
May 18 2022
paulson <lp15@cam.ac.uk> committed rAFPd859db6acb75: A tiny bit of reorganisation.
A tiny bit of reorganisation
paulson <lp15@cam.ac.uk> committed rISABELLE91c16c5ad3e9: tidied auto / simp with null arguments.
tidied auto / simp with null arguments
May 17 2022
May 17 2022
paulson <lp15@cam.ac.uk> committed rAFP3149eae9c077: the last "simp/auto" problems.
the last "simp/auto" problems
paulson <lp15@cam.ac.uk> committed rAFP58359778acff: corrected all "bysimp".
corrected all "bysimp"
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…
paulson <lp15@cam.ac.uk> committed rAFPef2cf009504d: Tidied auto/simp with null arguments.
Tidied auto/simp with null arguments
nipkow committed rAFP3ec6dc59412e: comleted single loop refinement.
comleted single loop refinement
May 16 2022
May 16 2022
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP613d8d8fb067: minor adjustments.
minor adjustments
user9716869 <user9716869@gmail.com> committed rAFPda39b5964de3: metadata.
metadata
user9716869 <user9716869@gmail.com> committed rAFPb4f4acb4ee94: minor amendments.
minor amendments
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…
May 13 2022
May 13 2022
Fabian Huch <huch@in.tum.de> committed rAFP00c034528a4a: clarified formatting, for the sake of scala3;.
clarified formatting, for the sake of scala3;
Fabian Huch <huch@in.tum.de> committed rAFPfbafb44dc503: hugo site: better scrolling;.
hugo site: better scrolling;
May 12 2022
May 12 2022
paulson <lp15@cam.ac.uk> committed rAFPa3f22844a82d: patched a broken proof.
patched a broken proof
nipkow committed rAFP8bcb5f82bf5b: single lopp variant refined to lists..
single lopp variant refined to lists.
May 11 2022
May 11 2022
provide Isabelle/Electron test;
May 10 2022
May 10 2022
paulson <lp15@cam.ac.uk> committed rAFPd7801c6a5adf: sitegen for Digit_Expansions.
sitegen for Digit_Expansions
adjust for isabelle@7095df141819
paulson <lp15@cam.ac.uk> committed rAFP143b4d24fbba: New entry Digit_Expansions.
New entry Digit_Expansions
paulson <lp15@cam.ac.uk> committed rAFPb11ab6e691fc: finally!!!! Sitegen for Sophomore's Dream.
finally!!!! Sitegen for Sophomore's Dream
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
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)
paulson <lp15@cam.ac.uk> committed rAFPee785c9dce1a: new entry Sophomores_Dream.
new entry Sophomores_Dream
paulson <lp15@cam.ac.uk> committed rAFPbf87ecbb9af7: updated metadata.
updated metadata
updated name and email address of Rose Bohrer
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP75635e4f695b: new entry Clique_and_Monotone_Circuits.
new entry Clique_and_Monotone_Circuits
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP05cff0f17aaf: sitegen for Clique_and_Monotone_Circuits.
sitegen for Clique_and_Monotone_Circuits
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1da45ba16d3e: new entry: Fisher's Inequality.
new entry: Fisher's Inequality
nipkow committed rAFP7c00f83aacff: New entry Multiset_Ordering_NPC.
New entry Multiset_Ordering_NPC
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa6a2db6744be: metadata and sitegen for Fisher's inequality.
metadata and sitegen for Fisher's inequality
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
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa108597c1ee8: new entry: Frequence_Moments.
new entry: Frequence_Moments
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP0f61fdaf00bf: sitegen for Frequence_Moments.
sitegen for Frequence_Moments
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP4895a13e16de: new entry: Prefix_Free_Code_Combinators.
new entry: Prefix_Free_Code_Combinators
regen website (some orders are different in python3)
switch sitegen to python3
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1de107e93d5c: sitegen for new entry.
sitegen for new entry
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP06b9a0364651: new entry: FOL_Seq_Calc3.
new entry: FOL_Seq_Calc3
nipkow committed rAFPe1c3276c598b: New entry: Dedekind_Real.
New entry: Dedekind_Real
paulson <lp15@cam.ac.uk> committed rAFP74cbc440d11b: Cotangent_PFD_Formula sitegen.
Cotangent_PFD_Formula sitegen
nipkow committed rAFPc296f652adc9: New entry Ackermann_not_PR, from distribution.
New entry Ackermann_not_PR, from distribution
paulson <lp15@cam.ac.uk> committed rAFPe08bf2dbf0e3: new entry Cotangent_PFD_Formula.
new entry Cotangent_PFD_Formula
paulson <lp15@cam.ac.uk> committed rAFPa304d5d49542: website for Independence_CH.
website for Independence_CH
paulson <lp15@cam.ac.uk> committed rAFPf0c701e6661f: new entry Independence_CH.
new entry Independence_CH
nipkow committed rAFPbf120ce6a2ff: New entry ResiduatedTransitionSystem.
New entry ResiduatedTransitionSystem
paulson <lp15@cam.ac.uk> committed rAFPdeb6c18fa953: Transitive_Models webpage.
Transitive_Models webpage
paulson <lp15@cam.ac.uk> committed rAFP6ed8e38ee242: new entry Transitive_Models.
new entry Transitive_Models
May 9 2022
May 9 2022
updated name and email address of Rose Bohrer
May 6 2022
May 6 2022
paulson <lp15@cam.ac.uk> committed rISABELLEf16d83de3e4a: Tidied up some super-messy proofs.
Tidied up some super-messy proofs
paulson <lp15@cam.ac.uk> committed rAFP6ae899d8db32: Removal of unnecessary material.
Removal of unnecessary material
paulson <lp15@cam.ac.uk> committed rISABELLE51e05af57455: Added a couple of obvious simprules.
Added a couple of obvious simprules
May 4 2022
May 4 2022
May 2 2022
May 2 2022
paulson <lp15@cam.ac.uk> committed rAFP0915660e2387: perfectly pointless streamlining.
perfectly pointless streamlining
Apr 30 2022
Apr 30 2022
paulson <lp15@cam.ac.uk> committed rAFP33748b892d11: More general definition of gcard.
More general definition of gcard
Apr 26 2022
Apr 26 2022
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…
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…
tuned signature: avoid problems with scala3;
proper indentation;
Apr 25 2022
Apr 25 2022
nipkow committed rAFP15a6b7cce9c7: refined one-loop version further.
refined one-loop version further
Apr 22 2022
Apr 22 2022
makarius committed rISABELLE331f96a67924: clarified management of interpreter threads: more generic;.
clarified management of interpreter threads: more generic;
clarified signature;
clarified signature;
clarified signature, based on hints by IntelliJ IDEA;
more robust: avoid partiality;
clarified signature;
clarified signature;
tuned --- avoid warnings in scala3;
clarified signature;
Apr 18 2022
Apr 18 2022
paulson <lp15@cam.ac.uk> committed rAFPb2708c764337: tidied up a few proofs.
tidied up a few proofs
Apr 13 2022
Apr 13 2022
paulson <lp15@cam.ac.uk> committed rAFPc74a55e029d0: A bit of beautification.
A bit of beautification
pass new option only to new version of E
Apr 12 2022
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 11 2022
Apr 11 2022