isabelle-dev  

Messages by Date

• 2016/09/27 Re: [isabelle-dev] Jenkins maintenance Lars Hupel
• 2016/09/25 Re: [isabelle-dev] More HOL-Analysis Lawrence Paulson
• 2016/09/24 Re: [isabelle-dev] Jenkins maintenance Makarius
• 2016/09/24 Re: [isabelle-dev] Jenkins maintenance Makarius
• 2016/09/24 Re: [isabelle-dev] Jenkins maintenance Lars Hupel
• 2016/09/24 Re: [isabelle-dev] Jenkins maintenance Makarius
• 2016/09/24 Re: [isabelle-dev] Jenkins maintenance Lars Hupel
• 2016/09/23 Re: [isabelle-dev] More HOL-Analysis Johannes Hölzl
• 2016/09/21 Re: [isabelle-dev] More HOL-Analysis Johannes Hölzl
• 2016/09/21 Re: [isabelle-dev] More HOL-Analysis Lawrence Paulson
• 2016/09/21 Re: [isabelle-dev] More HOL-Analysis Lawrence Paulson
• 2016/09/20 Re: [isabelle-dev] [isabelle] Reconciling FinFuns in Distro and AFP Florian Haftmann
• 2016/09/19 [isabelle-dev] NEWS: syntax for unique existence quantifier Makarius
• 2016/09/19 Re: [isabelle-dev] not-exists problem Makarius
• 2016/09/17 Re: [isabelle-dev] Jenkins maintenance Lars Hupel
• 2016/09/16 Re: [isabelle-dev] More HOL-Analysis Johannes Hölzl
• 2016/09/16 Re: [isabelle-dev] More HOL-Analysis Lawrence Paulson
• 2016/09/16 [isabelle-dev] More HOL-Analysis Makarius
• 2016/09/14 [isabelle-dev] NEWS: abbrevs and symbols dockable Makarius
• 2016/09/14 [isabelle-dev] Jenkins maintenance Lars Hupel
• 2016/09/14 Re: [isabelle-dev] not-exists problem Lawrence Paulson
• 2016/09/14 Re: [isabelle-dev] not-exists problem Tobias Nipkow
• 2016/09/14 Re: [isabelle-dev] not-exists problem Peter Lammich
• 2016/09/14 Re: [isabelle-dev] not-exists problem Michael.Norrish
• 2016/09/13 Re: [isabelle-dev] not-exists problem Jasmin Blanchette
• 2016/09/13 Re: [isabelle-dev] not-exists problem Lawrence Paulson
• 2016/09/13 Re: [isabelle-dev] not-exists problem Makarius
• 2016/09/13 Re: [isabelle-dev] not-exists problem Lawrence Paulson
• 2016/09/13 Re: [isabelle-dev] not-exists problem Manuel Eberl
• 2016/09/13 [isabelle-dev] Code Folding and errors Peter Lammich
• 2016/09/13 Re: [isabelle-dev] not-exists problem Johannes Hölzl
• 2016/09/13 Re: [isabelle-dev] not-exists problem Tjark Weber
• 2016/09/13 Re: [isabelle-dev] not-exists problem Tobias Nipkow
• 2016/09/13 Re: [isabelle-dev] not-exists problem Jasmin Blanchette
• 2016/09/13 Re: [isabelle-dev] not-exists problem Peter Lammich
• 2016/09/12 [isabelle-dev] not-exists problem Lawrence Paulson
• 2016/09/10 [isabelle-dev] Timeouts in AFP Lars Hupel
• 2016/09/08 [isabelle-dev] NEWS: system option "checkpoint" Makarius
• 2016/09/07 [isabelle-dev] NEWS: unfold_abs_def Makarius
• 2016/09/06 [isabelle-dev] Isabelle leap year release Makarius
• 2016/09/02 Re: [isabelle-dev] Status of HOL/Library/Old_SMT.thy Jasmin Blanchette
• 2016/09/01 [isabelle-dev] Status of HOL/Library/Old_SMT.thy Makarius
• 2016/09/01 [isabelle-dev] NEWS: isabelle.keymap-merge Makarius
• 2016/08/31 Re: [isabelle-dev] Problem with thm and meta-hypothesis Makarius
• 2016/08/31 [isabelle-dev] Problem with thm and meta-hypothesis Burkhart Wolff
• 2016/08/18 Re: [isabelle-dev] Z3_Proof_Reconstruction boehmes
• 2016/08/17 [isabelle-dev] Z3_Proof_Reconstruction Johannes Gareis
• 2016/08/16 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Makarius
• 2016/08/16 [isabelle-dev] Isabelle_15-Aug-2016 Makarius
• 2016/08/13 Re: [isabelle-dev] Theory for discrete log etc. Manuel Eberl
• 2016/08/13 [isabelle-dev] Theory for discrete log etc. Florian Haftmann
• 2016/08/11 Re: [isabelle-dev] comm_monoid, comm_monoid_set in bbcb05504fdc Florian Haftmann
• 2016/08/11 Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory Florian Haftmann
• 2016/08/10 [isabelle-dev] NEWS: split! Tobias Nipkow
• 2016/08/10 Re: [isabelle-dev] Build statistics Lars Hupel
• 2016/08/09 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Makarius
• 2016/08/09 Re: [isabelle-dev] NEWS: proof outline with cases Makarius
• 2016/08/08 Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis Makarius
• 2016/08/08 Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis Andreas Lochbihler
• 2016/08/08 Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis Johannes Hölzl
• 2016/08/08 Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis Lawrence Paulson
• 2016/08/08 [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis Johannes Hölzl
• 2016/08/08 Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory Bertram Felgenhauer
• 2016/08/08 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Lars Hupel
• 2016/08/08 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Makarius
• 2016/08/08 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Makarius
• 2016/08/08 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Lars Hupel
• 2016/08/08 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Tobias Nipkow
• 2016/08/08 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Manuel Eberl
• 2016/08/08 Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle Makarius
• 2016/08/08 Re: [isabelle-dev] NEWS: proof outline with cases Andreas Lochbihler
• 2016/08/07 [isabelle-dev] comm_monoid, comm_monoid_set in bbcb05504fdc Florian Haftmann
• 2016/08/05 [isabelle-dev] NEWS: more PIDE structure parsing Makarius
• 2016/08/02 [isabelle-dev] NEWS: abbrevs within theory header Makarius
• 2016/08/01 Re: [isabelle-dev] Multiset insert Jasmin Blanchette
• 2016/08/01 Re: [isabelle-dev] Multiset insert Bertram Felgenhauer
• 2016/07/29 Re: [isabelle-dev] jdk-8u102 Makarius
• 2016/07/28 Re: [isabelle-dev] NEWS: Primes Manuel Eberl
• 2016/07/28 [isabelle-dev] jdk-8u102 Makarius
• 2016/07/28 Re: [isabelle-dev] Multiset insert Jasmin Blanchette
• 2016/07/28 Re: [isabelle-dev] Multiset insert Manuel Eberl
• 2016/07/28 Re: [isabelle-dev] Multiset insert Florian Haftmann
• 2016/07/28 Re: [isabelle-dev] Multiset insert Florian Haftmann
• 2016/07/28 Re: [isabelle-dev] Multiset insert Tobias Nipkow
• 2016/07/28 Re: [isabelle-dev] Multiset insert Jasmin Blanchette
• 2016/07/28 Re: [isabelle-dev] Multiset insert Peter Lammich
• 2016/07/28 Re: [isabelle-dev] Multiset insert Jasmin Blanchette
• 2016/07/27 Re: [isabelle-dev] Multiset insert Tobias Nipkow
• 2016/07/27 Re: [isabelle-dev] Multiset insert Jasmin Blanchette
• 2016/07/27 Re: [isabelle-dev] NEWS: Primes Tobias Nipkow
• 2016/07/27 [isabelle-dev] NEWS: Primes Manuel Eberl
• 2016/07/27 Re: [isabelle-dev] Multiset insert Mathias Fleury
• 2016/07/26 Re: [isabelle-dev] Multiset insert Tobias Nipkow
• 2016/07/26 Re: [isabelle-dev] Multiset insert Mathias Fleury
• 2016/07/21 [isabelle-dev] PLATFORMS: Linux base-line is Ubuntu 12.04 LTS Makarius
• 2016/07/21 [isabelle-dev] NEWS: Makarius
• 2016/07/21 [isabelle-dev] NEWS: Proof methods "simp" and "simp_all" in Pure Makarius
• 2016/07/21 [isabelle-dev] NEWS: Proof method "use" in Pure Makarius
• 2016/07/19 Re: [isabelle-dev] \nexists Makarius
• 2016/07/19 Re: [isabelle-dev] multiplicity and prime numbers Manuel Eberl
• 2016/07/19 Re: [isabelle-dev] multiplicity and prime numbers Johannes Hölzl
• 2016/07/19 Re: [isabelle-dev] multiplicity and prime numbers Lawrence Paulson
• 2016/07/19 Re: [isabelle-dev] multiplicity and prime numbers Lawrence Paulson
• 2016/07/19 Re: [isabelle-dev] multiplicity and prime numbers Mario Carneiro
• 2016/07/19 Re: [isabelle-dev] multiplicity and prime numbers Manuel Eberl
• 2016/07/19 Re: [isabelle-dev] multiplicity and prime numbers Tobias Nipkow
• 2016/07/19 [isabelle-dev] multiplicity and prime numbers Manuel Eberl
• 2016/07/19 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/18 Re: [isabelle-dev] \nexists Makarius
• 2016/07/18 Re: [isabelle-dev] \nexists Makarius
• 2016/07/18 Re: [isabelle-dev] \nexists Joachim Breitner
• 2016/07/18 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/17 Re: [isabelle-dev] Build NEWS Lars Hupel
• 2016/07/16 Re: [isabelle-dev] Jenkins SPAM reduction Lars Hupel
• 2016/07/16 Re: [isabelle-dev] \nexists Makarius
• 2016/07/16 [isabelle-dev] Jenkins SPAM reduction Makarius
• 2016/07/16 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/16 Re: [isabelle-dev] \nexists Makarius
• 2016/07/16 Re: [isabelle-dev] \nexists Makarius
• 2016/07/16 [isabelle-dev] Broken AFP Manuel Eberl
• 2016/07/16 Re: [isabelle-dev] \nexists Tobias Nipkow
• 2016/07/16 [isabelle-dev] NEWS: proof outline with cases Makarius
• 2016/07/15 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/15 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/15 Re: [isabelle-dev] \nexists Joachim Breitner
• 2016/07/15 Re: [isabelle-dev] \nexists Makarius
• 2016/07/15 Re: [isabelle-dev] \nexists Makarius
• 2016/07/15 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/15 Re: [isabelle-dev] \nexists Tobias Nipkow
• 2016/07/15 Re: [isabelle-dev] \nexists Makarius
• 2016/07/15 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/15 Re: [isabelle-dev] \nexists Lars Hupel
• 2016/07/15 Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax Makarius
• 2016/07/15 Re: [isabelle-dev] \nexists Makarius
• 2016/07/15 Re: [isabelle-dev] \nexists Johannes Hölzl
• 2016/07/15 Re: [isabelle-dev] \nexists Johannes Hölzl
• 2016/07/15 Re: [isabelle-dev] \nexists Tobias Nipkow
• 2016/07/15 Re: [isabelle-dev] \nexists Makarius
• 2016/07/14 [isabelle-dev] \nexists Lawrence Paulson
• 2016/07/14 Re: [isabelle-dev] Use HTTPS for components Makarius
• 2016/07/14 Re: [isabelle-dev] Use HTTPS for components Makarius
• 2016/07/13 Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax Makarius
• 2016/07/13 Re: [isabelle-dev] Use HTTPS for components Makarius
• 2016/07/13 Re: [isabelle-dev] Use HTTPS for components Lawrence Paulson
• 2016/07/12 Re: [isabelle-dev] Use HTTPS for components Gerwin Klein
• 2016/07/12 [isabelle-dev] Use HTTPS for components Lars Hupel
• 2016/07/12 [isabelle-dev] NEWS: refined folding mode "isabelle" Makarius
• 2016/07/12 Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax Makarius
• 2016/07/12 Re: [isabelle-dev] Simplification theorems with more general typeclasses Mathias Fleury
• 2016/07/11 [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax Makarius
• 2016/07/11 Re: [isabelle-dev] {0::nat..<n} = {..<n} Florian Haftmann
• 2016/07/11 Re: [isabelle-dev] Considered harmful: surj Florian Haftmann
• 2016/07/11 Re: [isabelle-dev] Build NEWS Lars Hupel
• 2016/07/10 Re: [isabelle-dev] Build NEWS Andreas Lochbihler
• 2016/07/10 Re: [isabelle-dev] Build NEWS Gerwin Klein
• 2016/07/10 Re: [isabelle-dev] Build NEWS Johannes Hölzl
• 2016/07/10 [isabelle-dev] Build NEWS Lars Hupel
• 2016/07/08 [isabelle-dev] NEWS Tobias Nipkow
• 2016/07/06 Re: [isabelle-dev] An experience report on the testboard Lars Hupel
• 2016/07/05 Re: [isabelle-dev] Permutations Johannes Hölzl
• 2016/07/05 Re: [isabelle-dev] Permutations Florian Haftmann
• 2016/07/05 Re: [isabelle-dev] Permutations Johannes Hölzl
• 2016/07/05 Re: [isabelle-dev] {0::nat..<n} = {..<n} Florian Haftmann
• 2016/07/05 Re: [isabelle-dev] An experience report on the testboard Florian Haftmann
• 2016/07/05 Re: [isabelle-dev] Permutations Florian Haftmann
• 2016/07/05 Re: [isabelle-dev] Simplification theorems with more general typeclasses Mathias Fleury
• 2016/07/05 Re: [isabelle-dev] Permutations Johannes Hölzl
• 2016/07/05 Re: [isabelle-dev] Bijections Johannes Hölzl
• 2016/07/05 Re: [isabelle-dev] An experience report on the testboard Gerwin Klein
• 2016/07/04 Re: [isabelle-dev] {0::nat..<n} = {..<n} Andreas Röhler
• 2016/07/04 Re: [isabelle-dev] {0::nat..<n} = {..<n} Tobias Nipkow
• 2016/07/04 Re: [isabelle-dev] An experience report on the testboard Lars Hupel
• 2016/07/04 Re: [isabelle-dev] An experience report on the testboard Gerwin Klein
• 2016/07/04 Re: [isabelle-dev] An experience report on the testboard Lars Hupel
• 2016/07/04 Re: [isabelle-dev] An experience report on the testboard Lars Hupel
• 2016/07/04 [isabelle-dev] NEWS: "blast" is more robust Makarius
• 2016/07/04 [isabelle-dev] NEWS: literal facts Makarius
• 2016/07/04 [isabelle-dev] Permutations Florian Haftmann
• 2016/07/04 [isabelle-dev] Bijections Florian Haftmann
• 2016/07/04 Re: [isabelle-dev] An experience report on the testboard Florian Haftmann
• 2016/07/04 Re: [isabelle-dev] An experience report on the testboard Florian Haftmann
• 2016/07/04 Re: [isabelle-dev] {0::nat..<n} = {..<n} Florian Haftmann
• 2016/07/04 Re: [isabelle-dev] An experience report on the testboard Lars Hupel
• 2016/07/04 Re: [isabelle-dev] Simplification theorems with more general typeclasses Mathias Fleury
• 2016/07/04 Re: [isabelle-dev] Simplification theorems with more general typeclasses Johannes Hölzl
• 2016/07/04 Re: [isabelle-dev] Considered harmful: surj Johannes Hölzl
• 2016/07/03 Re: [isabelle-dev] {0::nat..<n} = {..<n} Tobias Nipkow
• 2016/07/02 Re: [isabelle-dev] An experience report on the testboard Lars Hupel
• 2016/07/02 [isabelle-dev] Considered harmful: surj Florian Haftmann
• 2016/07/02 [isabelle-dev] {0::nat..<n} = {..<n} Florian Haftmann
• 2016/07/02 [isabelle-dev] An experience report on the testboard Florian Haftmann
• 2016/07/01 Re: [isabelle-dev] Scala implicits Florian Haftmann
• 2016/06/28 [isabelle-dev] Simplification theorems with more general typeclasses Mathias Fleury
• 2016/06/23 Re: [isabelle-dev] AFP config files? Gerwin Klein
• 2016/06/23 Re: [isabelle-dev] Scala implicits Florian Haftmann
• 2016/06/23 Re: [isabelle-dev] Scala implicits Manuel Eberl
• 2016/06/23 Re: [isabelle-dev] Scala implicits Manuel Eberl
• 2016/06/23 Re: [isabelle-dev] AFP config files? Lars Hupel
• 2016/06/23 Re: [isabelle-dev] AFP config files? Manuel Eberl
• 2016/06/23 [isabelle-dev] AFP config files? Florian Haftmann

• Earlier messages
• Later messages