isabelle-dev
Thread
Date
Earlier messages
Later messages
Messages by Thread
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Lars Hupel
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Lawrence Paulson
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Florian Haftmann
[isabelle-dev] MIR decision procedure
Lawrence Paulson
Re: [isabelle-dev] MIR decision procedure
Tobias Nipkow
Re: [isabelle-dev] MIR decision procedure
Lawrence Paulson
Re: [isabelle-dev] MIR decision procedure
Amine Chaieb
Re: [isabelle-dev] MIR decision procedure
Lawrence Paulson
[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Japheth Lim
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Lars Hupel
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Japheth Lim
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Makarius
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Rafal Kolanski
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Makarius
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
Rafal Kolanski
[isabelle-dev] the function "real"
Lawrence Paulson
Re: [isabelle-dev] the function "real"
Manuel Eberl
Re: [isabelle-dev] the function "real"
Lawrence Paulson
Re: [isabelle-dev] the function "real"
Johannes Hölzl
Re: [isabelle-dev] the function "real"
Lawrence Paulson
Re: [isabelle-dev] the function "real"
Johannes Hölzl
Re: [isabelle-dev] the function "real"
Johannes Hölzl
Re: [isabelle-dev] the function "real"
Manuel Eberl
Re: [isabelle-dev] the function "real"
Lawrence Paulson
Re: [isabelle-dev] the function "real"
Tobias Nipkow
Re: [isabelle-dev] the function "real"
Lawrence Paulson
Re: [isabelle-dev] the function "real"
Tobias Nipkow
Re: [isabelle-dev] the function "real"
Florian Haftmann
Re: [isabelle-dev] the function "real"
Lawrence Paulson
Re: [isabelle-dev] the function "real"
Lars Noschinski
Re: [isabelle-dev] the function "real"
Lars Noschinski
Re: [isabelle-dev] the function "real"
Fabian Immler
Re: [isabelle-dev] the function "real"
Fabian Immler
[isabelle-dev] Jenkins testboard
Lars Hupel
[isabelle-dev] Isabelle/jEdit - Sidekick
Mathias Fleury
Re: [isabelle-dev] Isabelle/jEdit - Sidekick
Makarius
[isabelle-dev] NEWS: State panel
Makarius
Re: [isabelle-dev] NEWS: State panel
Mathias Fleury
Re: [isabelle-dev] NEWS: State panel
Makarius
Re: [isabelle-dev] NEWS: State panel
Gerwin Klein
Re: [isabelle-dev] NEWS: State panel
Tobias Nipkow
Re: [isabelle-dev] NEWS: State panel
Fabian Immler
Re: [isabelle-dev] NEWS: State panel
Makarius
[isabelle-dev] Non-responding Isabelle/jEdit and Monitor panel
Fabian Immler
Re: [isabelle-dev] Non-responding Isabelle/jEdit and Monitor panel
Makarius
Re: [isabelle-dev] Non-responding Isabelle/jEdit and Monitor panel
Makarius
[isabelle-dev] NEWS: undefined ML expression
Makarius
[isabelle-dev] NEWS: completion of explicit symbols
Makarius
[isabelle-dev] NEWS: timeout_scale
Makarius
[isabelle-dev] Towards the Isabelle release
Makarius
[isabelle-dev] real v of_nat
Lawrence Paulson
[isabelle-dev] Repository version of Isabelle on Windows 7
Anders Schlichtkrull
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Makarius
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Anders Schlichtkrull
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Makarius
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
Anders Schlichtkrull
[isabelle-dev] copy_bnf
Lars Hupel
Re: [isabelle-dev] copy_bnf
Dmitriy Traytel
Re: [isabelle-dev] copy_bnf
Lars Hupel
[isabelle-dev] Changes to the locale syntax
Clemens Ballarin
Re: [isabelle-dev] Changes to the locale syntax
Florian Haftmann
Re: [isabelle-dev] Changes to the locale syntax
Makarius
Re: [isabelle-dev] Changes to the locale syntax
Makarius
Re: [isabelle-dev] Changes to the locale syntax
Clemens Ballarin
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Clemens Ballarin
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Clemens Ballarin
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Makarius
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Clemens Ballarin
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
[isabelle-dev] Update of jdk and jedit components
Makarius
Re: [isabelle-dev] Update of jdk and jedit components
Mathias Fleury
Re: [isabelle-dev] Update of jdk and jedit components
Makarius
Re: [isabelle-dev] Update of jdk and jedit components
Mathias Fleury
Re: [isabelle-dev] Update of jdk and jedit components
Makarius
Re: [isabelle-dev] Update of jdk and jedit components
Dmitriy Traytel
Re: [isabelle-dev] Update of jdk and jedit components
Makarius
[isabelle-dev] isatest/afptest logs
Lars Hupel
Re: [isabelle-dev] isatest/afptest logs
Gerwin Klein
Re: [isabelle-dev] isatest/afptest logs
Makarius
[isabelle-dev] NEWS: editor reactivity and State panel
Makarius
[isabelle-dev] NEWS: document preparation refinements
Makarius
Re: [isabelle-dev] NEWS: document preparation refinements
Makarius
Re: [isabelle-dev] NEWS: document preparation refinements
Makarius
Re: [isabelle-dev] NEWS: document preparation refinements
Tobias Nipkow
Re: [isabelle-dev] NEWS: document preparation refinements
Makarius
Re: [isabelle-dev] NEWS: document preparation refinements
Tobias Nipkow
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Christian Sternagel
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Florian Haftmann
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Bertram Felgenhauer
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Florian Haftmann
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Jose Divasón
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Florian Haftmann
[isabelle-dev] Explicit option "open" for code_reflect
Frédéric Tuong
Re: [isabelle-dev] Explicit option "open" for code_reflect
Florian Haftmann
Re: [isabelle-dev] Explicit option "open" for code_reflect
Frédéric Tuong
Re: [isabelle-dev] Explicit option "open" for code_reflect
Florian Haftmann
[isabelle-dev] Mac OS X 10.11 (El Capitan)
Makarius
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
Larry Paulson
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
Makarius
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
Gerwin Klein
[isabelle-dev] Future of permanent_interpretation
Florian Haftmann
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
Re: [isabelle-dev] Future of permanent_interpretation
Tobias Nipkow
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
Re: [isabelle-dev] Future of permanent_interpretation
Tobias Nipkow
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
Re: [isabelle-dev] Future of permanent_interpretation
Makarius
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
Re: [isabelle-dev] Future of permanent_interpretation
Clemens Ballarin
Re: [isabelle-dev] Future of permanent_interpretation
Florian Haftmann
[isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]
Florian Haftmann
Re: [isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]
Clemens Ballarin
Re: [isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]
Florian Haftmann
Re: [isabelle-dev] Future of permanent_interpretation
Tobias Nipkow
[isabelle-dev] New testing infrastructure
Lars Hupel
Re: [isabelle-dev] New testing infrastructure
Lars Hupel
[isabelle-dev] local ghc and happy installations in Munich
Lars Noschinski
[isabelle-dev] Broken AFP sessions
Makarius
Re: [isabelle-dev] Broken AFP sessions
Dmitriy Traytel
Re: [isabelle-dev] Broken AFP sessions
Larry Paulson
Re: [isabelle-dev] Broken AFP sessions
Makarius
[isabelle-dev] NEWS: toplevel theorem statements
Makarius
Re: [isabelle-dev] NEWS: toplevel theorem statements
Tobias Nipkow
Re: [isabelle-dev] NEWS: toplevel theorem statements
Lawrence Paulson
Re: [isabelle-dev] NEWS: toplevel theorem statements
Makarius
[isabelle-dev] http://isabelle.in.tum.de/reports/Isabelle
Makarius
Re: [isabelle-dev] http://isabelle.in.tum.de/reports/Isabelle
Lars Hupel
[isabelle-dev] HOL-Proofs broken?
Makarius
Re: [isabelle-dev] HOL-Proofs broken?
Jasmin Blanchette
Re: [isabelle-dev] HOL-Proofs broken?
Dmitriy Traytel
Re: [isabelle-dev] HOL-Proofs broken?
Makarius
Re: [isabelle-dev] HOL-Proofs broken?
Makarius
Re: [isabelle-dev] HOL-Proofs broken?
Jasmin Blanchette
Re: [isabelle-dev] HOL-Proofs broken?
Jasmin Blanchette
[isabelle-dev] Scrollbar, where are thou?
Dmitriy Traytel
Re: [isabelle-dev] Scrollbar, where are thou?
Makarius
Re: [isabelle-dev] Scrollbar, where are thou?
Makarius
[isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2
Dmitriy Traytel
Re: [isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2
Jasmin Blanchette
[isabelle-dev] AFP/Lifting_Definition_Option
Makarius
Re: [isabelle-dev] AFP/Lifting_Definition_Option
Gerwin Klein
Re: [isabelle-dev] AFP/Lifting_Definition_Option
Ondřej Kunčar
Re: [isabelle-dev] AFP/Lifting_Definition_Option
Gerwin Klein
[isabelle-dev] real, of_nat and Suc
Larry Paulson
[isabelle-dev] NEWS: Thm.pretty_thm etc.
Makarius
[isabelle-dev] NEWS: definitional typedef
Makarius
[isabelle-dev] Notes on GHC an mutable data structures
Florian Haftmann
Re: [isabelle-dev] Notes on GHC an mutable data structures
Makarius
[isabelle-dev] Exposing some functions of the API
Frédéric Tuong
Re: [isabelle-dev] Exposing some functions of the API
Florian Haftmann
Re: [isabelle-dev] Exposing some functions of the API
Jasmin Blanchette
Re: [isabelle-dev] Exposing some functions of the API
Frédéric Tuong
Re: [isabelle-dev] Exposing some functions of the API
Makarius
Re: [isabelle-dev] Exposing some functions of the API
Makarius
[isabelle-dev] JinjaThreads
Makarius
Re: [isabelle-dev] JinjaThreads
Andreas Lochbihler
Re: [isabelle-dev] JinjaThreads
Andreas Lochbihler
[isabelle-dev] NEWS: HOL/Library/Omega_Words_Fun
Peter Lammich
Re: [isabelle-dev] NEWS: HOL/Library/Omega_Words_Fun
Makarius
Re: [isabelle-dev] [isabelle] Code setup for Fraction_Field
Andreas Lochbihler
[isabelle-dev] ML equality types
Florian Haftmann
Re: [isabelle-dev] ML equality types
Larry Paulson
Re: [isabelle-dev] ML equality types
Makarius
Re: [isabelle-dev] ML equality types
Florian Haftmann
Re: [isabelle-dev] ML equality types
Lars Hupel
[isabelle-dev] HOL-Predicate_Compile_Examples
Makarius
Re: [isabelle-dev] HOL-Predicate_Compile_Examples
Andreas Lochbihler
Re: [isabelle-dev] HOL-Predicate_Compile_Examples
Makarius
[isabelle-dev] Code generation to OCaml and Scala
Frédéric Tuong
Re: [isabelle-dev] Code generation to OCaml and Scala
Florian Haftmann
Re: [isabelle-dev] Code generation to OCaml and Scala
Florian Haftmann
Re: [isabelle-dev] Code generation to OCaml and Scala
Frédéric Tuong
[isabelle-dev] State of affairs with simplifier tracing?
Florian Haftmann
Re: [isabelle-dev] State of affairs with simplifier tracing?
Makarius
[isabelle-dev] simps_of_case and function types
Lars Noschinski
Re: [isabelle-dev] simps_of_case and function types
Lars Noschinski
Re: [isabelle-dev] simps_of_case and function types
Lars Hupel
[isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Rafal Kolanski
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Makarius
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Rafal Kolanski
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Makarius
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Makarius
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Rafal Kolanski
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Makarius
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Rafal Kolanski
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Makarius
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
Rafal Kolanski
Re: [isabelle-dev] status (AFP)
Larry Paulson
Re: [isabelle-dev] status (AFP)
Gerwin Klein
[isabelle-dev] NEWS: updated to jdk-8u60, with support for x86_64-windows
Makarius
[isabelle-dev] NEWS: IDE support for the source-level debugger of Poly/ML
Makarius
Earlier messages
Later messages