isabelle-dev
Thread
Date
Earlier messages
Later messages
Messages by Thread
Re: [isabelle-dev] Sum of Squares server down?
Makarius
Re: [isabelle-dev] Sum of Squares server down?
Makarius
Re: [isabelle-dev] Sum of Squares server down?
Lawrence Paulson
Re: [isabelle-dev] Sum of Squares server down?
Tobias Nipkow
Re: [isabelle-dev] Sum of Squares server down?
Tobias Nipkow
[isabelle-dev] NEWS: "class_deps" with optional search space constraints
Florian Haftmann
Re: [isabelle-dev] NEWS: "class_deps" with optional search space constraints
Tobias Nipkow
Re: [isabelle-dev] NEWS: "class_deps" with optional search space constraints
Dmitriy Traytel
[isabelle-dev] Towards datatype_new ~> datatype
Jasmin Christian Blanchette
Re: [isabelle-dev] Towards datatype_new ~> datatype
Jasmin Christian Blanchette
[isabelle-dev] duplicate fact in List
Christian Sternagel
Re: [isabelle-dev] duplicate fact in List
Tobias Nipkow
[isabelle-dev] Proposal for localized interpretations
Jasmin Christian Blanchette
Re: [isabelle-dev] Proposal for localized interpretations
Florian Haftmann
Re: [isabelle-dev] Proposal for localized interpretations
Jasmin Christian Blanchette
Re: [isabelle-dev] Proposal for localized interpretations
Florian Haftmann
Re: [isabelle-dev] Proposal for localized interpretations
Makarius
Re: [isabelle-dev] Proposal for localized interpretations
Makarius
Re: [isabelle-dev] Proposal for localized interpretations
Makarius
Re: [isabelle-dev] Proposal for localized interpretations
Andreas Lochbihler
Re: [isabelle-dev] Proposal for localized interpretations
Florian Haftmann
Re: [isabelle-dev] Proposal for localized interpretations
Makarius
Re: [isabelle-dev] Proposal for localized interpretations
Jasmin Christian Blanchette
Re: [isabelle-dev] Proposal for localized interpretations
Florian Haftmann
[isabelle-dev] default cases rule
Christian Sternagel
Re: [isabelle-dev] default cases rule
Dmitriy Traytel
Re: [isabelle-dev] default cases rule
Jasmin Christian Blanchette
Re: [isabelle-dev] default cases rule
Christian Sternagel
Re: [isabelle-dev] default cases rule
Makarius
[isabelle-dev] Problem with type inference in locale expressions
Florian Haftmann
Re: [isabelle-dev] Problem with type inference in locale expressions
Clemens Ballarin
Re: [isabelle-dev] Problem with type inference in locale expressions
Florian Haftmann
Re: [isabelle-dev] Problem with type inference in locale expressions
Florian Haftmann
Re: [isabelle-dev] Problem with type inference in locale expressions
Clemens Ballarin
Re: [isabelle-dev] Problem with type inference in locale expressions
Florian Haftmann
Re: [isabelle-dev] Problem with type inference in locale expressions
Florian Haftmann
[isabelle-dev] Diagnostic value command
Florian Haftmann
[isabelle-dev] NEWS
Jasmin Christian Blanchette
[isabelle-dev] NEWS
Florian Haftmann
Re: [isabelle-dev] NEWS
Dmitriy Traytel
Re: [isabelle-dev] NEWS
Florian Haftmann
Re: [isabelle-dev] NEWS
Tobias Nipkow
Re: [isabelle-dev] NEWS
Larry Paulson
Re: [isabelle-dev] NEWS
Makarius
Re: [isabelle-dev] NEWS
Lars Noschinski
[isabelle-dev] Definite name for case combinator on products [was: NEWS]
Florian Haftmann
Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]
Dmitriy Traytel
Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]
Florian Haftmann
Re: [isabelle-dev] NEWS
Andreas Lochbihler
Re: [isabelle-dev] NEWS
Florian Haftmann
Re: [isabelle-dev] NEWS
Tobias Nipkow
Re: [isabelle-dev] NEWS
Florian Haftmann
[isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]
Florian Haftmann
Re: [isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]
Tobias Nipkow
Re: [isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]
Larry Paulson
Re: [isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]
Florian Haftmann
Re: [isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]
Makarius
[isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Florian Haftmann
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Larry Paulson
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Tobias Nipkow
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Florian Haftmann
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Makarius
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Michael Norrish
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Tobias Nipkow
[isabelle-dev] NEWS
Ondřej Kunčar
Re: [isabelle-dev] NEWS
Andreas Lochbihler
[isabelle-dev] NEWS
Lawrence Paulson
Re: [isabelle-dev] NEWS
Makarius
[isabelle-dev] NEWS
Florian Haftmann
[isabelle-dev] NEWS
Florian Haftmann
[isabelle-dev] NEWS
Tobias Nipkow
[isabelle-dev] NEWS
Lawrence Paulson
[isabelle-dev] NEWS
Lawrence Paulson
[isabelle-dev] NEWS
Florian Haftmann
Re: [isabelle-dev] NEWS
Lars Hupel
Re: [isabelle-dev] NEWS
Florian Haftmann
Re: [isabelle-dev] NEWS
Lars Hupel
Re: [isabelle-dev] NEWS
Makarius
Re: [isabelle-dev] NEWS
Makarius
[isabelle-dev] Testing of generated code
Andreas Lochbihler
Re: [isabelle-dev] Testing of generated code
Makarius
Re: [isabelle-dev] Testing of generated code
Andreas Lochbihler
Re: [isabelle-dev] Testing of generated code
Florian Haftmann
Re: [isabelle-dev] Testing of generated code
Makarius
Re: [isabelle-dev] Testing of generated code
Florian Haftmann
[isabelle-dev] porting code to isabelle2014 and getting "unfinished linear change" errors
Michael Norrish
Re: [isabelle-dev] porting code to isabelle2014 and getting "unfinished linear change" errors
Lars Noschinski
Re: [isabelle-dev] porting code to isabelle2014 and getting "unfinished linear change" errors
Michael Norrish
Re: [isabelle-dev] porting code to isabelle2014 and getting "unfinished linear change" errors
Michael Norrish
Re: [isabelle-dev] porting code to isabelle2014 and getting "unfinished linear change" errors
Gerwin Klein
[isabelle-dev] afp-2014 fork
Gerwin Klein
Re: [isabelle-dev] afp-2014 fork
Makarius
Re: [isabelle-dev] afp-2014 fork
Gerwin Klein
[isabelle-dev] RDP 2015 Call for Workshops
Aleksy Schubert
Re: [isabelle-dev] RDP 2015 Call for Workshops
Makarius
[isabelle-dev] Fwd: [isabelle] seL4 open source
Florian Haftmann
Re: [isabelle-dev] Fwd: [isabelle] seL4 open source
Gerwin Klein
[isabelle-dev] Haskabelle test
Lars Noschinski
Re: [isabelle-dev] Haskabelle test
Florian Haftmann
Re: [isabelle-dev] looping continues in the background
Makarius
Re: [isabelle-dev] looping continues in the background
Makarius
[isabelle-dev] Website – Link to Narkive from Isabelle User Mailing List is broken
Florian Haftmann
Re: [isabelle-dev] Website – Link to Narkive from Isabelle User Mailing List is broken
Makarius
Re: [isabelle-dev] Website – Link to Narkive from Isabelle User Mailing List is broken
Makarius
[isabelle-dev] ISABELLE_GHC/quickcheck
Gerwin Klein
Re: [isabelle-dev] ISABELLE_GHC/quickcheck
Florian Haftmann
Re: [isabelle-dev] ISABELLE_GHC/quickcheck
Gerwin Klein
Re: [isabelle-dev] ISABELLE_GHC/quickcheck
Andreas Lochbihler
Re: [isabelle-dev] ISABELLE_GHC/quickcheck
Gerwin Klein
Re: [isabelle-dev] ISABELLE_GHC/quickcheck
Makarius
[isabelle-dev] datatype_new problem
Christian Sternagel
Re: [isabelle-dev] datatype_new problem
Christian Sternagel
Re: [isabelle-dev] datatype_new problem
Jasmin Christian Blanchette
[isabelle-dev] show "A ==> B"
Askar Safin
Re: [isabelle-dev] *** Spam *** show "A ==> B"
Makarius
Re: [isabelle-dev] show "A ==> B"
Brian Huffman
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Florian Haftmann
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Lawrence Paulson
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Andreas Lochbihler
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Tobias Nipkow
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Andreas Lochbihler
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Tobias Nipkow
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Andreas Lochbihler
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Tobias Nipkow
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Peter Lammich
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Andreas Lochbihler
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Makarius
[isabelle-dev] Old 'defs'
Makarius
Re: [isabelle-dev] Old 'defs'
Florian Haftmann
Re: [isabelle-dev] Old 'defs'
Andreas Lochbihler
Re: [isabelle-dev] Old 'defs'
Makarius
[isabelle-dev] sledgehammer "problem malformed" message
Leo Freitas
Re: [isabelle-dev] sledgehammer "problem malformed" message
Jasmin Christian Blanchette
Re: [isabelle-dev] sledgehammer "problem malformed" message
Jasmin Christian Blanchette
[isabelle-dev] Methods that fail with stack-overflow
Peter Lammich
Re: [isabelle-dev] Methods that fail with stack-overflow
Lars Noschinski
Re: [isabelle-dev] Methods that fail with stack-overflow
Makarius
Re: [isabelle-dev] Methods that fail with stack-overflow
Dmitriy Traytel
Re: [isabelle-dev] Methods that fail with stack-overflow
Tobias Nipkow
Re: [isabelle-dev] Methods that fail with stack-overflow
Johannes Hölzl
Re: [isabelle-dev] Methods that fail with stack-overflow
Makarius
[isabelle-dev] Bad state of repository
Makarius
Re: [isabelle-dev] Bad state of repository
Jasmin Christian Blanchette
Re: [isabelle-dev] Notes and updates on Isabelle/ML
Makarius
Re: [isabelle-dev] Notes and updates on Isabelle/ML
Jasmin Christian Blanchette
[isabelle-dev] pull request (HOL-Library/Sublist(_Order))
Christian Sternagel
Re: [isabelle-dev] pull request (HOL-Library/Sublist(_Order))
Florian Haftmann
Re: [isabelle-dev] pull request (HOL-Library/Sublist(_Order))
Florian Haftmann
Re: [isabelle-dev] pull request (HOL-Library/Sublist(_Order))
Christian Sternagel
[isabelle-dev] NEWS: Proof General is now an optional component
Makarius
[isabelle-dev] NEWS: "isabelle tty" is superseded by "isabelle console"
Makarius
[isabelle-dev] Product on lists
Florian Haftmann
[isabelle-dev] Code preprocessor tracing
Florian Haftmann
Re: [isabelle-dev] Code preprocessor tracing
Andreas Lochbihler
Re: [isabelle-dev] Code preprocessor tracing
Florian Haftmann
Re: [isabelle-dev] Code preprocessor tracing
Andreas Lochbihler
Re: [isabelle-dev] JinjaThreads CYCLES-Exception at export-code
Florian Haftmann
[isabelle-dev] Theory_Data.extend still needed?
Florian Haftmann
Re: [isabelle-dev] Theory_Data.extend still needed?
Makarius
[isabelle-dev] NEWS: Updated and extended manuals
Makarius
[isabelle-dev] JEdit FAILED
Florian Haftmann
Re: [isabelle-dev] JEdit FAILED
Makarius
Re: [isabelle-dev] JEdit FAILED
Florian Haftmann
Re: [isabelle-dev] JEdit FAILED
Makarius
Re: [isabelle-dev] JEdit FAILED
Makarius
Re: [isabelle-dev] JEdit FAILED
Lars Noschinski
Re: [isabelle-dev] JEdit FAILED
Florian Haftmann
[isabelle-dev] Error highlighting in ML for @{lemma}
Lars Noschinski
Re: [isabelle-dev] Error highlighting in ML for @{lemma}
Makarius
[isabelle-dev] Isabelle/jedit reports that file was changed on disk
Clemens Ballarin
Re: [isabelle-dev] Isabelle/jedit reports that file was changed on disk
Makarius
[isabelle-dev] jdk-7u60
Makarius
[isabelle-dev] Problems with datatype-new
René Thiemann
Re: [isabelle-dev] Problems with datatype-new
Dmitriy Traytel
Re: [isabelle-dev] Problems with datatype-new
Jasmin Christian Blanchette
[isabelle-dev] AFP: Failing entries
Peter Lammich
Re: [isabelle-dev] AFP: Failing entries
Gerwin Klein
Re: [isabelle-dev] AFP: Failing entries
Peter Lammich
Re: [isabelle-dev] AFP: Failing entries
Gerwin Klein
Re: [isabelle-dev] [isabelle] Code_Abstract_Nat raises exception for a variable with name g
Florian Haftmann
Re: [isabelle-dev] [isabelle] Code_Abstract_Nat raises exception for a variable with name g
Florian Haftmann
[isabelle-dev] Build problems in AFP with current tips
Florian Haftmann
Re: [isabelle-dev] Build problems in AFP with current tips
Lawrence Paulson
Re: [isabelle-dev] Build problems in AFP with current tips
Florian Haftmann
Re: [isabelle-dev] Build problems in AFP with current tips
Florian Haftmann
Re: [isabelle-dev] Build problems in AFP with current tips
Johannes Hölzl
[isabelle-dev] NEWS: enabled MaSh by default
Jasmin Christian Blanchette
[isabelle-dev] NEWS: enabled MaSh by default
Jasmin Christian Blanchette
[isabelle-dev] Help
Adamu sani yahaya
Re: [isabelle-dev] Help
John Wickerson
Re: [isabelle-dev] Help
Makarius
[isabelle-dev] export_code theory wildcard exports too much
René Neumann
Re: [isabelle-dev] export_code theory wildcard exports too much
Florian Haftmann
[isabelle-dev] Fwd: [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Dmitriy Traytel
Re: [isabelle-dev] [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Gerwin Klein
[isabelle-dev] White space in theory names
Florian Haftmann
Re: [isabelle-dev] White space in theory names
Makarius
[isabelle-dev] transfer with integers needs including / not documented in NEWS
René Neumann
[isabelle-dev] AFP failures near 7f7ca3a43026
Florian Haftmann
Re: [isabelle-dev] AFP failures near 7f7ca3a43026
Gerwin Klein
Earlier messages
Later messages