Messages by Date
-
2015/12/01
Re: [isabelle-dev] MIR decision procedure
Lawrence Paulson
-
2015/12/01
Re: [isabelle-dev] MIR decision procedure
Amine Chaieb
-
2015/11/30
Re: [isabelle-dev] Infinite_Set.thy
Lawrence Paulson
-
2015/11/27
Re: [isabelle-dev] Infinite_Set.thy
Tobias Nipkow
-
2015/11/27
[isabelle-dev] Infinite_Set.thy
Lawrence Paulson
-
2015/11/26
Re: [isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
-
2015/11/26
Re: [isabelle-dev] find_theorems and type class axioms
Johannes Hölzl
-
2015/11/26
Re: [isabelle-dev] find_theorems and type class axioms
Andreas Lochbihler
-
2015/11/26
Re: [isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
-
2015/11/26
Re: [isabelle-dev] find_theorems and type class axioms
Florian Haftmann
-
2015/11/26
Re: [isabelle-dev] popup in ce6320b9ef9b
Florian Haftmann
-
2015/11/26
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Florian Haftmann
-
2015/11/23
Re: [isabelle-dev] Immediate completion does not work anymore
Manuel Eberl
-
2015/11/22
Re: [isabelle-dev] Immediate completion does not work anymore
Makarius
-
2015/11/19
Re: [isabelle-dev] find_theorems and type class axioms
Gerwin Klein
-
2015/11/19
[isabelle-dev] Immediate completion does not work anymore
Manuel Eberl
-
2015/11/19
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
-
2015/11/19
Re: [isabelle-dev] Future of isatest/afptest
Lars Hupel
-
2015/11/19
Re: [isabelle-dev] Future of isatest/afptest
Peter Gammie
-
2015/11/19
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Makarius
-
2015/11/19
Re: [isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Lammich
-
2015/11/19
Re: [isabelle-dev] find_theorems and type class axioms
Manuel Eberl
-
2015/11/19
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Lawrence Paulson
-
2015/11/19
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Lawrence Paulson
-
2015/11/19
Re: [isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
-
2015/11/19
Re: [isabelle-dev] popup in ce6320b9ef9b
Lars Hupel
-
2015/11/19
Re: [isabelle-dev] popup in ce6320b9ef9b
Florian Haftmann
-
2015/11/19
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Lammich
-
2015/11/19
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Florian Haftmann
-
2015/11/19
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Lars Hupel
-
2015/11/19
Re: [isabelle-dev] find_theorems and type class axioms
Andreas Lochbihler
-
2015/11/19
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Florian Haftmann
-
2015/11/19
Re: [isabelle-dev] find_theorems and type class axioms
Florian Haftmann
-
2015/11/18
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Jasmin Blanchette
-
2015/11/18
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
-
2015/11/18
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Clemens Ballarin
-
2015/11/18
[isabelle-dev] Future of isatest/afptest
Lars Hupel
-
2015/11/18
[isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Lawrence Paulson
-
2015/11/18
Re: [isabelle-dev] extra lemmas
Lawrence Paulson
-
2015/11/18
[isabelle-dev] popup in ce6320b9ef9b
Tobias Nipkow
-
2015/11/17
Re: [isabelle-dev] test failed (Archive of Formal Proofs)
Peter Gammie
-
2015/11/17
Re: [isabelle-dev] test failed (Archive of Formal Proofs)
Peter Gammie
-
2015/11/17
Re: [isabelle-dev] test failed (Archive of Formal Proofs)
Lars Hupel
-
2015/11/16
[isabelle-dev] extra lemmas
Peter Gammie
-
2015/11/16
[isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
-
2015/11/16
Re: [isabelle-dev] CGSCreateKeyboardEvent
Lawrence Paulson
-
2015/11/16
Re: [isabelle-dev] the function "real"
Lars Noschinski
-
2015/11/16
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Johannes Hölzl
-
2015/11/15
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Rafal Kolanski
-
2015/11/15
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Rafal Kolanski
-
2015/11/15
Re: [isabelle-dev] Isabelle/jEdit - Sidekick
Makarius
-
2015/11/15
[isabelle-dev] CGSCreateKeyboardEvent
Makarius
-
2015/11/15
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Makarius
-
2015/11/15
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Gammie
-
2015/11/15
[isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Gammie
-
2015/11/15
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Andreas Lochbihler
-
2015/11/15
Re: [isabelle-dev] the function "real"
Florian Haftmann
-
2015/11/15
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
-
2015/11/15
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Florian Haftmann
-
2015/11/15
[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Florian Haftmann
-
2015/11/14
Re: [isabelle-dev] Changes to the locale syntax
Makarius
-
2015/11/14
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Makarius
-
2015/11/13
Re: [isabelle-dev] MIR decision procedure
Lawrence Paulson
-
2015/11/13
Re: [isabelle-dev] MIR decision procedure
Tobias Nipkow
-
2015/11/13
[isabelle-dev] MIR decision procedure
Lawrence Paulson
-
2015/11/12
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Rafal Kolanski
-
2015/11/12
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Japheth Lim
-
2015/11/12
Re: [isabelle-dev] the function "real"
Tobias Nipkow
-
2015/11/12
Re: [isabelle-dev] the function "real"
Lawrence Paulson
-
2015/11/12
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Makarius
-
2015/11/12
Re: [isabelle-dev] the function "real"
Tobias Nipkow
-
2015/11/12
Re: [isabelle-dev] the function "real"
Lars Noschinski
-
2015/11/12
Re: [isabelle-dev] the function "real"
Lawrence Paulson
-
2015/11/12
Re: [isabelle-dev] the function "real"
Lawrence Paulson
-
2015/11/12
Re: [isabelle-dev] the function "real"
Fabian Immler
-
2015/11/12
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Lars Hupel
-
2015/11/12
Re: [isabelle-dev] the function "real"
Fabian Immler
-
2015/11/12
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Jose Divasón
-
2015/11/12
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Florian Haftmann
-
2015/11/12
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
-
2015/11/12
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
-
2015/11/12
Re: [isabelle-dev] the function "real"
Manuel Eberl
-
2015/11/11
[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Japheth Lim
-
2015/11/11
Re: [isabelle-dev] the function "real"
Johannes Hölzl
-
2015/11/11
Re: [isabelle-dev] the function "real"
Johannes Hölzl
-
2015/11/11
Re: [isabelle-dev] the function "real"
Lawrence Paulson
-
2015/11/11
Re: [isabelle-dev] the function "real"
Johannes Hölzl
-
2015/11/11
Re: [isabelle-dev] the function "real"
Lawrence Paulson
-
2015/11/11
Re: [isabelle-dev] Non-responding Isabelle/jEdit and Monitor panel
Makarius
-
2015/11/11
[isabelle-dev] Non-responding Isabelle/jEdit and Monitor panel
Fabian Immler
-
2015/11/10
Re: [isabelle-dev] the function "real"
Manuel Eberl
-
2015/11/10
[isabelle-dev] the function "real"
Lawrence Paulson
-
2015/11/10
[isabelle-dev] Jenkins testboard
Lars Hupel
-
2015/11/10
Re: [isabelle-dev] NEWS: State panel
Tobias Nipkow
-
2015/11/10
Re: [isabelle-dev] NEWS: State panel
Fabian Immler
-
2015/11/10
Re: [isabelle-dev] NEWS: State panel
Gerwin Klein
-
2015/11/10
Re: [isabelle-dev] NEWS: State panel
Mathias Fleury
-
2015/11/10
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Anders Schlichtkrull
-
2015/11/10
[isabelle-dev] Isabelle/jEdit - Sidekick
Mathias Fleury
-
2015/11/09
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Makarius
-
2015/11/09
[isabelle-dev] NEWS: State panel
Makarius
-
2015/11/09
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
-
2015/11/09
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Anders Schlichtkrull
-
2015/11/09
Re: [isabelle-dev] Future of permanent_interpretation
Makarius
-
2015/11/08
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
-
2015/11/08
[isabelle-dev] NEWS: undefined ML expression
Makarius
-
2015/11/08
[isabelle-dev] NEWS: completion of explicit symbols
Makarius
-
2015/11/08
[isabelle-dev] NEWS: timeout_scale
Makarius
-
2015/11/07
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
-
2015/11/07
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Bertram Felgenhauer
-
2015/11/06
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
-
2015/11/04
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
-
2015/11/04
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Clemens Ballarin
-
2015/11/04
Re: [isabelle-dev] Changes to the locale syntax
Clemens Ballarin
-
2015/11/04
Re: [isabelle-dev] Update of jdk and jedit components
Makarius
-
2015/11/04
Re: [isabelle-dev] Update of jdk and jedit components
Mathias Fleury
-
2015/11/04
[isabelle-dev] Towards the Isabelle release
Makarius
-
2015/11/04
Re: [isabelle-dev] Update of jdk and jedit components
Makarius
-
2015/11/04
Re: [isabelle-dev] Update of jdk and jedit components
Mathias Fleury
-
2015/11/02
[isabelle-dev] real v of_nat
Lawrence Paulson
-
2015/10/30
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
-
2015/10/30
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Makarius
-
2015/10/30
[isabelle-dev] Repository version of Isabelle on Windows 7
Anders Schlichtkrull
-
2015/10/30
Re: [isabelle-dev] Changes to the locale syntax
Makarius
-
2015/10/29
Re: [isabelle-dev] Explicit option "open" for code_reflect
Florian Haftmann
-
2015/10/29
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Florian Haftmann
-
2015/10/29
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
-
2015/10/29
Re: [isabelle-dev] copy_bnf
Lars Hupel
-
2015/10/29
Re: [isabelle-dev] copy_bnf
Dmitriy Traytel
-
2015/10/29
[isabelle-dev] copy_bnf
Lars Hupel
-
2015/10/29
Re: [isabelle-dev] Future of permanent_interpretation
Tobias Nipkow
-
2015/10/29
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
-
2015/10/29
Re: [isabelle-dev] Changes to the locale syntax
Florian Haftmann
-
2015/10/29
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
-
2015/10/29
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
-
2015/10/28
Re: [isabelle-dev] Future of permanent_interpretation
Tobias Nipkow
-
2015/10/28
[isabelle-dev] Changes to the locale syntax
Clemens Ballarin
-
2015/10/28
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
-
2015/10/27
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Clemens Ballarin
-
2015/10/26
Re: [isabelle-dev] NEWS: document preparation refinements
Makarius
-
2015/10/26
Re: [isabelle-dev] NEWS: document preparation refinements
Tobias Nipkow
-
2015/10/26
Re: [isabelle-dev] NEWS: document preparation refinements
Makarius
-
2015/10/26
Re: [isabelle-dev] Future of permanent_interpretation
Tobias Nipkow
-
2015/10/25
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
-
2015/10/24
Re: [isabelle-dev] NEWS: document preparation refinements
Tobias Nipkow
-
2015/10/23
[isabelle-dev] Update of jdk and jedit components
Makarius
-
2015/10/23
Re: [isabelle-dev] NEWS: document preparation refinements
Makarius
-
2015/10/20
Re: [isabelle-dev] isatest/afptest logs
Makarius
-
2015/10/20
Re: [isabelle-dev] isatest/afptest logs
Gerwin Klein
-
2015/10/20
[isabelle-dev] isatest/afptest logs
Lars Hupel
-
2015/10/19
[isabelle-dev] NEWS: editor reactivity and State panel
Makarius
-
2015/10/19
[isabelle-dev] NEWS: document preparation refinements
Makarius
-
2015/10/19
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Christian Sternagel
-
2015/10/15
Re: [isabelle-dev] Explicit option "open" for code_reflect
Frédéric Tuong
-
2015/10/15
Re: [isabelle-dev] Explicit option "open" for code_reflect
Florian Haftmann
-
2015/10/14
Re: [isabelle-dev] New testing infrastructure
Lars Hupel
-
2015/10/13
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
Gerwin Klein
-
2015/10/13
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
Makarius
-
2015/10/13
[isabelle-dev] Explicit option "open" for code_reflect
Frédéric Tuong
-
2015/10/13
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
Larry Paulson
-
2015/10/13
[isabelle-dev] Mac OS X 10.11 (El Capitan)
Makarius
-
2015/10/13
[isabelle-dev] Future of permanent_interpretation
Florian Haftmann
-
2015/10/13
Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]
Florian Haftmann
-
2015/10/12
[isabelle-dev] New testing infrastructure
Lars Hupel
-
2015/10/11
Re: [isabelle-dev] NEWS: toplevel theorem statements
Makarius
-
2015/10/11
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Tobias Nipkow
-
2015/10/11
Re: [isabelle-dev] NEWS: toplevel theorem statements
Lawrence Paulson
-
2015/10/10
Re: [isabelle-dev] NEWS: toplevel theorem statements
Tobias Nipkow
-
2015/10/09
[isabelle-dev] local ghc and happy installations in Munich
Lars Noschinski
-
2015/10/09
Re: [isabelle-dev] NEWS
Andreas Lochbihler
-
2015/10/08
[isabelle-dev] NEWS
Ondřej Kunčar
-
2015/10/07
Re: [isabelle-dev] AFP/Lifting_Definition_Option
Gerwin Klein
-
2015/10/07
Re: [isabelle-dev] Scrollbar, where are thou?
Makarius
-
2015/10/07
Re: [isabelle-dev] Broken AFP sessions
Makarius
-
2015/10/07
Re: [isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]
Makarius
-
2015/10/07
Re: [isabelle-dev] AFP/Lifting_Definition_Option
Ondřej Kunčar
-
2015/10/07
Re: [isabelle-dev] Broken AFP sessions
Larry Paulson
-
2015/10/07
Re: [isabelle-dev] HOL-Proofs broken?
Jasmin Blanchette
-
2015/10/07
Re: [isabelle-dev] Broken AFP sessions
Dmitriy Traytel
-
2015/10/06
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Michael Norrish
-
2015/10/06
[isabelle-dev] Broken AFP sessions
Makarius
-
2015/10/06
Re: [isabelle-dev] HOL-Proofs broken?
Jasmin Blanchette
-
2015/10/06
Re: [isabelle-dev] HOL-Proofs broken?
Makarius
-
2015/10/06
Re: [isabelle-dev] HOL-Proofs broken?
Makarius
-
2015/10/06
Re: [isabelle-dev] HOL-Proofs broken?
Dmitriy Traytel
-
2015/10/06
Re: [isabelle-dev] http://isabelle.in.tum.de/reports/Isabelle
Lars Hupel
-
2015/10/06
Re: [isabelle-dev] HOL-Proofs broken?
Jasmin Blanchette
-
2015/10/06
[isabelle-dev] NEWS: toplevel theorem statements
Makarius
-
2015/10/06
[isabelle-dev] http://isabelle.in.tum.de/reports/Isabelle
Makarius
-
2015/10/06
[isabelle-dev] HOL-Proofs broken?
Makarius
-
2015/10/06
Re: [isabelle-dev] Notes on GHC an mutable data structures
Makarius
-
2015/10/06
Re: [isabelle-dev] Scrollbar, where are thou?
Makarius
-
2015/10/06
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Makarius
-
2015/10/06
[isabelle-dev] Scrollbar, where are thou?
Dmitriy Traytel
-
2015/10/06
Re: [isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2
Jasmin Blanchette
-
2015/10/06
[isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2
Dmitriy Traytel
-
2015/10/06
Re: [isabelle-dev] Exposing some functions of the API
Makarius
-
2015/10/05
Re: [isabelle-dev] Exposing some functions of the API
Frédéric Tuong
-
2015/10/05
Re: [isabelle-dev] AFP/Lifting_Definition_Option
Gerwin Klein
-
2015/10/05
Re: [isabelle-dev] Exposing some functions of the API
Makarius