isabelle-dev
Thread
Date
Earlier messages
Later messages
Messages by Thread
[isabelle-dev] Status of afp-devel wrt. release?
Makarius
Re: [isabelle-dev] Status of afp-devel wrt. release?
Gerwin Klein
[isabelle-dev] "Subgoal" command and meta-conjunctions
Daniel Matichuk
Re: [isabelle-dev] "Subgoal" command and meta-conjunctions
Makarius
[isabelle-dev] New mailing list: isabelle-ci
Lars Hupel
Re: [isabelle-dev] [isabelle] Disk usage in ~/.isabelle/contrib
Matthew Fernandez
Re: [isabelle-dev] [isabelle] Disk usage in ~/.isabelle/contrib
Makarius
Re: [isabelle-dev] [isabelle] Disk usage in ~/.isabelle/contrib
Matthew Fernandez
[isabelle-dev] Mail on build failures
Lars Hupel
Re: [isabelle-dev] Mail on build failures
Gerwin Klein
Re: [isabelle-dev] Mail on build failures
Florian Haftmann
[isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Makarius
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lawrence Paulson
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Makarius
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Makarius
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Makarius
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Florian Haftmann
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Jasmin Blanchette
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Makarius
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Jasmin Blanchette
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Makarius
Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
[isabelle-dev] Maintenance work on Jenkins VM
Lars Hupel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Dmitriy Traytel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Lars Hupel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Lars Hupel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Dmitriy Traytel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Lars Hupel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Lars Hupel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Lars Hupel
Re: [isabelle-dev] Maintenance work on Jenkins VM
Andreas Lochbihler
Re: [isabelle-dev] Maintenance work on Jenkins VM
Andreas Lochbihler
Re: [isabelle-dev] Maintenance work on Jenkins VM
Lars Hupel
[isabelle-dev] jdk-8u72
Makarius
[isabelle-dev] Regression in Approximation – Does this belong into NEWS?
Manuel Eberl
Re: [isabelle-dev] Regression in Approximation – Does this belong into NEWS?
Makarius
[isabelle-dev] Multicore timings
Makarius
Re: [isabelle-dev] Multicore timings
Gerwin Klein
Re: [isabelle-dev] Multicore timings
Lawrence Paulson
Re: [isabelle-dev] Multicore timings
Makarius
[isabelle-dev] next release
Lawrence Paulson
Re: [isabelle-dev] next release
Thomas Sewell
[isabelle-dev] Localized record package [was: next release]
Florian Haftmann
Re: [isabelle-dev] Localized record package [was: next release]
Makarius
Re: [isabelle-dev] Localized record package [was: next release]
Makarius
Re: [isabelle-dev] next release
Makarius
Re: [isabelle-dev] next release
Thomas Sewell
[isabelle-dev] NEWS: better resource usage on all platforms
Makarius
[isabelle-dev] AFP status
Makarius
Re: [isabelle-dev] AFP status
Andreas Lochbihler
Re: [isabelle-dev] AFP status
Manuel Eberl
Re: [isabelle-dev] Impossible_Geometry
Johannes Hölzl
[isabelle-dev] HOL-Codegenerator_Test error
Lawrence Paulson
Re: [isabelle-dev] HOL-Codegenerator_Test error
Manuel Eberl
Re: [isabelle-dev] HOL-Codegenerator_Test error
Makarius
Re: [isabelle-dev] HOL-Codegenerator_Test error
Lars Hupel
Re: [isabelle-dev] HOL-Codegenerator_Test error
Manuel Eberl
Re: [isabelle-dev] HOL-Codegenerator_Test error
Andreas Lochbihler
Re: [isabelle-dev] HOL-Codegenerator_Test error
Lars Hupel
Re: [isabelle-dev] HOL-Codegenerator_Test error
Manuel Eberl
Re: [isabelle-dev] HOL-Codegenerator_Test error
Lawrence Paulson
Re: [isabelle-dev] HOL-Codegenerator_Test error
Makarius
Re: [isabelle-dev] HOL-Codegenerator_Test error
Manuel Eberl
Re: [isabelle-dev] HOL-Codegenerator_Test error
Makarius
Re: [isabelle-dev] HOL-Codegenerator_Test error
Florian Haftmann
[isabelle-dev] Isabelle2016-RC0: potential changes
Thiemann, Rene
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Manuel Eberl
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Thiemann, Rene
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Manuel Eberl
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Thiemann, Rene
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Manuel Eberl
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Thiemann, Rene
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Manuel Eberl
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Makarius
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Florian Haftmann
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Thiemann, Rene
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Florian Haftmann
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Makarius
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Thiemann, Rene
Re: [isabelle-dev] semiring_gcd [was: Isabelle2016-RC0: potential changes]
Florian Haftmann
Re: [isabelle-dev] semiring_gcd [was: Isabelle2016-RC0: potential changes]
Thiemann, Rene
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Makarius
[isabelle-dev] NEWS: print_record
Gerwin Klein
[isabelle-dev] Line breaks in pretty-printed output
Tobias Nipkow
Re: [isabelle-dev] Line breaks in pretty-printed output
Makarius
Re: [isabelle-dev] Line breaks in pretty-printed output
Makarius
[isabelle-dev] Problem with code generation for non-executable types
Johannes Hölzl
Re: [isabelle-dev] Problem with code generation for non-executable types
Johannes Hölzl
Re: [isabelle-dev] Problem with code generation for non-executable types
Andreas Lochbihler
Re: [isabelle-dev] Problem with code generation for non-executable types
Johannes Hölzl
Re: [isabelle-dev] Problem with code generation for non-executable types
Florian Haftmann
Re: [isabelle-dev] Problem with code generation for non-executable types
Johannes Hölzl
Re: [isabelle-dev] Problem with code generation for non-executable types
Florian Haftmann
Re: [isabelle-dev] Problem with code generation for non-executable types
Johannes Hölzl
[isabelle-dev] CONTRIBUTIONS: The central limit theorem is now in Isabelle
Johannes Hölzl
Re: [isabelle-dev] CONTRIBUTIONS: The central limit theorem is now in Isabelle
Makarius
[isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Lawrence Paulson
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Manuel Eberl
Re: [isabelle-dev] Towards the release
Manuel Eberl
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Manuel Eberl
Re: [isabelle-dev] Towards the release
Johannes Hölzl
Re: [isabelle-dev] Towards the release
Lawrence Paulson
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
[isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Florian Haftmann
Re: [isabelle-dev] Towards the release
Manuel Eberl
Re: [isabelle-dev] Towards the release
Lawrence Paulson
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Jasmin Blanchette
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Simon Cruanes
Re: [isabelle-dev] Towards the release
Jasmin Blanchette
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Gerwin.Klein
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Lawrence Paulson
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Makarius
Re: [isabelle-dev] Towards the release
Gerwin.Klein
[isabelle-dev] Towards the release
Makarius
[isabelle-dev] Lemmas about tranclp and lexn
Mathias Fleury
Re: [isabelle-dev] Lemmas about tranclp and lexn
Tobias Nipkow
[isabelle-dev] CoreC++ broken
Makarius
Re: [isabelle-dev] CoreC++ broken
Andreas Lochbihler
[isabelle-dev] NEWS: print mode ASCII vs. xsymbols
Makarius
Re: [isabelle-dev] NEWS: print mode ASCII vs. xsymbols
Makarius
[isabelle-dev] Isabelle_23-Dec-2015
Makarius
Re: [isabelle-dev] Isabelle_23-Dec-2015
Florian Haftmann
[isabelle-dev] Spontaneous disappearance of a fixed variable
Florian Haftmann
[isabelle-dev] Towards the Isabelle2016 release
Makarius
Re: [isabelle-dev] Towards the Isabelle2016 release
Jasmin Blanchette
Re: [isabelle-dev] Towards the Isabelle2016 release
Florian Haftmann
[isabelle-dev] NEWS: fundamental PIDE GUI changes
Makarius
[isabelle-dev] Robust Windows support
Makarius
Re: [isabelle-dev] Robust Windows support
Alfio Martini
[isabelle-dev] Build problems in AFP
Florian Haftmann
Re: [isabelle-dev] Build problems in AFP
Lawrence Paulson
[isabelle-dev] Infinite_Set.thy
Lawrence Paulson
Re: [isabelle-dev] Infinite_Set.thy
Tobias Nipkow
Re: [isabelle-dev] Infinite_Set.thy
Lawrence Paulson
[isabelle-dev] Immediate completion does not work anymore
Manuel Eberl
Re: [isabelle-dev] Immediate completion does not work anymore
Makarius
Re: [isabelle-dev] Immediate completion does not work anymore
Manuel Eberl
[isabelle-dev] Future of isatest/afptest
Lars Hupel
Re: [isabelle-dev] Future of isatest/afptest
Peter Gammie
Re: [isabelle-dev] Future of isatest/afptest
Lars Hupel
Re: [isabelle-dev] Future of isatest/afptest
Lars Hupel
[isabelle-dev] popup in ce6320b9ef9b
Tobias Nipkow
Re: [isabelle-dev] popup in ce6320b9ef9b
Florian Haftmann
Re: [isabelle-dev] popup in ce6320b9ef9b
Lars Hupel
Re: [isabelle-dev] popup in ce6320b9ef9b
Florian Haftmann
Re: [isabelle-dev] test failed (Archive of Formal Proofs)
Peter Gammie
Re: [isabelle-dev] test failed (Archive of Formal Proofs)
Lars Hupel
Re: [isabelle-dev] test failed (Archive of Formal Proofs)
Peter Gammie
[isabelle-dev] extra lemmas
Peter Gammie
Re: [isabelle-dev] extra lemmas
Lawrence Paulson
[isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
Re: [isabelle-dev] find_theorems and type class axioms
Florian Haftmann
Re: [isabelle-dev] find_theorems and type class axioms
Andreas Lochbihler
Re: [isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
Re: [isabelle-dev] find_theorems and type class axioms
Manuel Eberl
Re: [isabelle-dev] find_theorems and type class axioms
Gerwin Klein
Re: [isabelle-dev] find_theorems and type class axioms
Florian Haftmann
Re: [isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
Re: [isabelle-dev] find_theorems and type class axioms
Andreas Lochbihler
Re: [isabelle-dev] find_theorems and type class axioms
Johannes Hölzl
Re: [isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
Re: [isabelle-dev] find_theorems and type class axioms
Florian Haftmann
Re: [isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
[isabelle-dev] CGSCreateKeyboardEvent
Makarius
Re: [isabelle-dev] CGSCreateKeyboardEvent
Lawrence Paulson
[isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Gammie
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Gammie
[isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Lawrence Paulson
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Jasmin Blanchette
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Florian Haftmann
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Lammich
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Lawrence Paulson
Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Makarius
Re: [isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
Peter Lammich
[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Florian Haftmann
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Andreas Lochbihler
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Johannes Hölzl
Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
Florian Haftmann
Earlier messages
Later messages