isabelle-dev
Thread
Date
Earlier messages
Messages by Thread
[isabelle-dev] Testboard and AFP
Lawrence Paulson
Re: [isabelle-dev] Testboard and AFP
Fabian Huch
Re: [isabelle-dev] Testboard and AFP
Tobias Nipkow
Re: [isabelle-dev] Testboard and AFP
Fabian Huch
Re: [isabelle-dev] Last minute acknowledgement
Makarius
[isabelle-dev] Isabelle2024-RC2 (18-Apr-2024): fork-point of the development repository
Makarius
Re: [isabelle-dev] Isabelle2024-RC2 (18-Apr-2024): fork-point of the development repository
Makarius
Re: [isabelle-dev] Isabelle2024-RC2 (18-Apr-2024): fork-point of the development repository
Makarius
Re: [isabelle-dev] Isabelle2024-RC2 (18-Apr-2024): fork-point of the development repository
Makarius
Re: [isabelle-dev] Isabelle2024-RC2 (18-Apr-2024): fork-point of the development repository
Makarius
Re: [isabelle-dev] Isabelle2024-RC2 (18-Apr-2024): fork-point of the development repository
Gerwin Klein
Re: [isabelle-dev] Isabelle2024-RC2 (18-Apr-2024): fork-point of the development repository
Makarius
[isabelle-dev] NEWS: isabelle go_setup
Makarius
Re: [isabelle-dev] NEWS: isabelle go_setup
Makarius
Re: [isabelle-dev] NEWS: isabelle go_setup
Makarius
Re: [isabelle-dev] NEWS: isabelle go_setup
Makarius
Re: [isabelle-dev] NEWS: isabelle go_setup
Fabian Huch
Re: [isabelle-dev] NEWS: isabelle go_setup
Makarius
[isabelle-dev] Admin/components/README.md
Makarius
Re: [isabelle-dev] Admin/components/README.md
Makarius
[isabelle-dev] Towards Isabelle2024-RC1
Makarius
Re: [isabelle-dev] Towards Isabelle2024-RC1
Makarius
Re: [isabelle-dev] Towards Isabelle2024-RC1
Makarius
[isabelle-dev] Timing for AFP/CakeML_Codegen
Makarius
Re: [isabelle-dev] Timing for AFP/CakeML_Codegen
Tobias Nipkow
Re: [isabelle-dev] Timing for AFP/CakeML_Codegen
Makarius
Re: [isabelle-dev] Timing for AFP/CakeML_Codegen
Tobias Nipkow
[isabelle-dev] 20 years of AFP
Fabian Huch
Re: [isabelle-dev] 20 years of AFP
Fabian Huch
Re: [isabelle-dev] 20 years of AFP
Makarius
Re: [isabelle-dev] 20 years of AFP
Fabian Huch
Re: [isabelle-dev] 20 years of AFP
Tobias Nipkow
[isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Lawrence Paulson
Re: [isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Jasmin Blanchette
Re: [isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Lawrence Paulson
Re: [isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Peter Lammich
Re: [isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Makarius
Re: [isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Manuel Eberl
Re: [isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Lawrence Paulson
Re: [isabelle-dev] Mercurial on lxbroy10.informatik.tu-muenchen.de
Manuel Eberl
[isabelle-dev] Something wrong with lxbroy10.informatik.tu-muenchen.de?
Lawrence Paulson
[isabelle-dev] Isabelle2024-RC0: Issue with LargeInt.int <> int unification
Joshua K .
Re: [isabelle-dev] Isabelle2024-RC0: Issue with LargeInt.int <> int unification
Makarius
[isabelle-dev] Failure of AFP/Polylog
Makarius
Re: [isabelle-dev] Failure of AFP/Polylog
Lawrence Paulson
Re: [isabelle-dev] Failure of AFP/Polylog
Makarius
[isabelle-dev] Script characters in words
Lawrence Paulson
Re: [isabelle-dev] Script characters in words
Makarius
Re: [isabelle-dev] Script characters in words
Makarius
Re: [isabelle-dev] Script characters in words
Tobias Nipkow
Re: [isabelle-dev] Script characters in words
Makarius
[isabelle-dev] Testboard timeout
Jasmin Blanchette
Re: [isabelle-dev] Testboard timeout
Fabian Huch
Re: [isabelle-dev] Testboard timeout
Tobias Nipkow
[isabelle-dev] Update to scala-3.3.3
Makarius
[isabelle-dev] e-3.0.03 available for testing
Makarius
[isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Makarius
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Makarius
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Tobias Nipkow
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Makarius
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Makarius
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Fabian Huch
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Fabian Immler
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Makarius
Re: [isabelle-dev] AFP: "enable proof in session Lorenz_C1"^
Makarius
[isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] Proven support for Linux ARM64
Jasmin Blanchette
Re: [isabelle-dev] Proven support for Linux ARM64
Lawrence Paulson
Re: [isabelle-dev] Proven support for Linux ARM64
Jasmin Blanchette
Re: [isabelle-dev] Proven support for Linux ARM64
Lawrence Paulson
Re: [isabelle-dev] Proven support for Linux ARM64
Florian Haftmann
Re: [isabelle-dev] Proven support for Linux ARM64
Jasmin Blanchette
Re: [isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] Proven support for Linux ARM64
Jasmin Blanchette
Re: [isabelle-dev] Proven support for Linux ARM64
Jasmin Blanchette
Re: [isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] Proven support for Linux ARM64
Jasmin Blanchette
Re: [isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] Proven support for Linux ARM64
Haniel Barbosa
Re: [isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] Proven support for Linux ARM64
Haniel Barbosa
Re: [isabelle-dev] Proven support for Linux ARM64
Haniel Barbosa
Re: [isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] Proven support for Linux ARM64
Makarius
Re: [isabelle-dev] [isabelle] Relaxing type class constraints on interval multiplication (HOL-Library.Interval)
Lawrence Paulson
[isabelle-dev] Update to OpenJDK 21.0.2
Makarius
[isabelle-dev] Plan for Isabelle2024 release
Makarius
Re: [isabelle-dev] Plan for Isabelle2024 release
Makarius
[isabelle-dev] Digitology: Leading the Digital Revolution in Egypt - Your Ultimate Choice for Digital Marketing Excellence
seo 2023
[isabelle-dev] NEWS: Update to OpenJDK 21
Makarius
Re: [isabelle-dev] NEWS: Update to OpenJDK 21
Makarius
[isabelle-dev] Session builds with threads>1 but never terminates for threads=1
Fabian Huch
Re: [isabelle-dev] Session builds with threads>1 but never terminates for threads=1
Lawrence Paulson
[isabelle-dev] HOL-ex.Sketch_and_Explore
Lawrence Paulson
Re: [isabelle-dev] HOL-ex.Sketch_and_Explore
Simon Wimmer
Re: [isabelle-dev] HOL-ex.Sketch_and_Explore
Lawrence Paulson
Re: [isabelle-dev] HOL-ex.Sketch_and_Explore
Makarius
Re: [isabelle-dev] HOL-ex.Sketch_and_Explore
Lawrence Paulson
[isabelle-dev] NEWS: Update of GHC stack with full support for ARM64 platforms
Makarius
[isabelle-dev] NEWS: Discontinuation of very old Linux and macOS versions
Makarius
[isabelle-dev] ML: distinguish proper interrupts from Poly/ML RTS breakdown
Makarius
[isabelle-dev] Is the distribution broken?
Lawrence Paulson
Re: [isabelle-dev] Is the distribution broken?
Martin Desharnais
[isabelle-dev] NEWS: Robust handling of program exceptions in Isabelle/ML
Makarius
[isabelle-dev] Pink tactics
Jasmin Blanchette
Re: [isabelle-dev] Pink tactics
Makarius
Re: [isabelle-dev] Pink tactics
Makarius
Re: [isabelle-dev] Pink tactics
Makarius
[isabelle-dev] Status of Isabelle "go" component
Makarius
[isabelle-dev] Latex problem on the AFP
Anders Schlichtkrull
Re: [isabelle-dev] Latex problem on the AFP
Achim D. Brucker
Re: [isabelle-dev] Latex problem on the AFP
Anders Schlichtkrull
Re: [isabelle-dev] Latex problem on the AFP
Makarius
Re: [isabelle-dev] Latex problem on the AFP
Anders Schlichtkrull
Re: [isabelle-dev] Latex problem on the AFP
Lawrence Paulson
[isabelle-dev] Isabelle2023-RC3 release fork today
Makarius
Re: [isabelle-dev] Isabelle2023-RC3 release fork today
Makarius
Re: [isabelle-dev] Isabelle2023-RC3 release fork today
Makarius
[isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Makarius
Re: [isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Makarius
Re: [isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Makarius
Re: [isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Makarius
Re: [isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Gerwin Klein
Re: [isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Makarius
Re: [isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Gerwin Klein
Re: [isabelle-dev] Towards Isabelle2023-RC2, RC3 and AFP release
Makarius
[isabelle-dev] Release Candidates for Isabelle2023
Makarius
[isabelle-dev] quickcheck throws "Type unification failed: No type arity t :: full_exhaustive" on simple example
Fabian Huch
Re: [isabelle-dev] quickcheck throws "Type unification failed: No type arity t :: full_exhaustive" on simple example
Jasmin Blanchette
[isabelle-dev] NEWS: significantly reduced ML heap usage
Makarius
Re: [isabelle-dev] NEWS: significantly reduced ML heap usage
Makarius
Re: [isabelle-dev] NEWS: significantly reduced ML heap usage
Lawrence Paulson
[isabelle-dev] Proposal to add a new \<notapprox> symbol and corresponding glyph to the Isabelle font
Martin Desharnais
Re: [isabelle-dev] Proposal to add a new \<notapprox> symbol and corresponding glyph to the Isabelle font
Lawrence Paulson
[isabelle-dev] Update to jdk-17.0.7
Makarius
[isabelle-dev] Towards the Isabelle2023 release
Makarius
[isabelle-dev] AFP: PAPP_Impossibility not terminating
Makarius
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Fabian Huch
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Makarius
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Manuel Eberl
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Makarius
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Manuel Eberl
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Makarius
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Makarius
Re: [isabelle-dev] AFP: PAPP_Impossibility not terminating
Makarius
Re: [isabelle-dev] Sous-traitance Isabelle_DOF
Burkhart Wolff
[isabelle-dev] Problem in AFP
Florian Haftmann
Re: [isabelle-dev] Problem in AFP
Makarius
Re: [isabelle-dev] Problem in AFP
Tobias Nipkow
Re: [isabelle-dev] Problem in AFP
Florian Haftmann
[isabelle-dev] Application of method algebra fails
christian
Re: [isabelle-dev] Application of method algebra fails
christian
[isabelle-dev] Two new experimental features in Sledgehammer
Jasmin Blanchette
Re: [isabelle-dev] Two new experimental features in Sledgehammer
Tobias Nipkow
Re: [isabelle-dev] Two new experimental features in Sledgehammer
Jasmin Blanchette
Re: [isabelle-dev] Two new experimental features in Sledgehammer
Tobias Nipkow
Re: [isabelle-dev] Two new experimental features in Sledgehammer
Tobias Nipkow
Re: [isabelle-dev] Two new experimental features in Sledgehammer
Jasmin Blanchette
[isabelle-dev] Function package creates duplicate simp rule
Fabian Huch
[isabelle-dev] Update to OpenJDK 17.0.6
Makarius
[isabelle-dev] Error in "cite" anitquotation
Lawrence Paulson
Re: [isabelle-dev] Error in "cite" anitquotation
Makarius
Re: [isabelle-dev] Error in "cite" anitquotation
Lawrence Paulson
Re: [isabelle-dev] Error in "cite" anitquotation
Makarius
[isabelle-dev] HOL/Library/BigO.thy
Lawrence Paulson
Re: [isabelle-dev] HOL/Library/BigO.thy
Tobias Nipkow
Re: [isabelle-dev] HOL/Library/BigO.thy
Makarius
Re: [isabelle-dev] HOL/Library/BigO.thy
Makarius
Re: [isabelle-dev] HOL/Library/BigO.thy
Gerwin Klein
Re: [isabelle-dev] HOL/Library/BigO.thy
Tobias Nipkow
Re: [isabelle-dev] HOL/Library/BigO.thy
Lawrence Paulson
Re: [isabelle-dev] HOL/Library/BigO.thy
Makarius
Re: [isabelle-dev] HOL/Library/BigO.thy
Lawrence Paulson
Re: [isabelle-dev] HOL/Library/BigO.thy
Makarius
Re: [isabelle-dev] HOL/Library/BigO.thy
Lawrence Paulson
Re: [isabelle-dev] HOL/Library/BigO.thy
Makarius
[isabelle-dev] NEWS: Support for interactive document preparation in PIDE
Makarius
[isabelle-dev] Update to jdk-17.0.5 (Oct-2022)
Makarius
[isabelle-dev] Update to scala-3.2.1
Makarius
[isabelle-dev] lemma top_empty_eq should not have attribute pred_set_conv
Martin Desharnais
Re: [isabelle-dev] lemma top_empty_eq should not have attribute pred_set_conv
Tobias Nipkow
Re: [isabelle-dev] lemma top_empty_eq should not have attribute pred_set_conv
Martin Desharnais
[isabelle-dev] Syntax highlighting for approx. 300 languages via Prism.js
Makarius
[isabelle-dev] From name string to Sledgehammer_Fact.fact_override
Albert Jiang
[isabelle-dev] Fossil SCM (SQLite)
Makarius
Re: [isabelle-dev] Fossil SCM (SQLite)
Urban, Christian
[isabelle-dev] NEWS: Demo documents for well-known LaTeX styles
Makarius
Re: [isabelle-dev] NEWS: Demo documents for well-known LaTeX styles
Tobias Nipkow
Re: [isabelle-dev] NEWS: Demo documents for well-known LaTeX styles
Jørgen Villadsen
Re: [isabelle-dev] NEWS: Demo documents for well-known LaTeX styles
Makarius
Re: [isabelle-dev] NEWS: Demo documents for well-known LaTeX styles
Jørgen Villadsen
[isabelle-dev] NEWS: Zstd compression for Isabelle/Scala and Isabelle/ML
Makarius
Re: [isabelle-dev] NEWS: Zstd compression for Isabelle/Scala and Isabelle/ML
Makarius
Re: [isabelle-dev] NEWS: Zstd compression for Isabelle/Scala and Isabelle/ML
Makarius
Re: [isabelle-dev] [isabelle] Suggestions for src/HOL/Fun.thy
Lawrence Paulson
[isabelle-dev] Isabelle2022-RC3 after repository fork
Makarius
[isabelle-dev] Isabelle2022-RC3 with repository fork: Sunday 02-Oct-2022 12:00 UTC
Makarius
Re: [isabelle-dev] Isabelle2022-RC3 with repository fork: Sunday 02-Oct-2022 12:00 UTC
Peter Lammich
Re: [isabelle-dev] Isabelle2022-RC3 with repository fork: Sunday 02-Oct-2022 12:00 UTC
Makarius
Earlier messages