Messages by Date
-
2015/06/06
Re: [isabelle-dev] Remaining uses of defer_recdef?
Larry Paulson
-
2015/06/06
Re: [isabelle-dev] Remaining uses of defer_recdef?
Tobias Nipkow
-
2015/06/06
Re: [isabelle-dev] »real« considered harmful
Larry Paulson
-
2015/06/06
Re: [isabelle-dev] Remaining uses of defer_recdef?
Larry Paulson
-
2015/06/06
Re: [isabelle-dev] Remaining uses of defer_recdef?
Florian Haftmann
-
2015/06/06
Re: [isabelle-dev] »real« considered harmful
Florian Haftmann
-
2015/06/06
Re: [isabelle-dev] Remaining uses of defer_recdef?
Tobias Nipkow
-
2015/06/06
Re: [isabelle-dev] Remaining uses of defer_recdef?
Makarius
-
2015/06/05
Re: [isabelle-dev] »real« considered harmful
Larry Paulson
-
2015/06/05
Re: [isabelle-dev] Remaining uses of defer_recdef?
Larry Paulson
-
2015/06/05
Re: [isabelle-dev] »real« considered harmful
Florian Haftmann
-
2015/06/05
Re: [isabelle-dev] »real« considered harmful
Florian Haftmann
-
2015/06/05
Re: [isabelle-dev] »real« considered harmful
Florian Haftmann
-
2015/06/05
Re: [isabelle-dev] Remaining uses of defer_recdef?
Florian Haftmann
-
2015/06/05
Re: [isabelle-dev] Infix syntax for division?
Florian Haftmann
-
2015/06/03
[isabelle-dev] Remaining uses of defer_recdef?
Makarius
-
2015/06/03
Re: [isabelle-dev] »real« considered harmful
Larry Paulson
-
2015/06/03
Re: [isabelle-dev] »real« considered harmful
Johannes Hölzl
-
2015/06/03
Re: [isabelle-dev] »real« considered harmful
Tobias Nipkow
-
2015/06/03
Re: [isabelle-dev] »real« considered harmful
Fabian Immler
-
2015/06/03
Re: [isabelle-dev] »real« considered harmful
Tobias Nipkow
-
2015/06/03
Re: [isabelle-dev] Infix syntax for division?
Tobias Nipkow
-
2015/06/02
Re: [isabelle-dev] Infix syntax for division?
Manuel Eberl
-
2015/06/02
Re: [isabelle-dev] Infix syntax for division?
Florian Haftmann
-
2015/06/02
Re: [isabelle-dev] Infix syntax for division?
Jasmin Blanchette
-
2015/06/02
Re: [isabelle-dev] Infix syntax for division?
Larry Paulson
-
2015/06/02
Re: [isabelle-dev] »real« considered harmful
Larry Paulson
-
2015/06/02
[isabelle-dev] »real« considered harmful
Florian Haftmann
-
2015/06/02
[isabelle-dev] Infix syntax for division?
Florian Haftmann
-
2015/05/28
Re: [isabelle-dev] Infinite loops with output
Makarius
-
2015/05/28
Re: [isabelle-dev] Infinite loops with output
Aymeric Bouzy
-
2015/05/28
Re: [isabelle-dev] Infinite loops with output
Makarius
-
2015/05/28
[isabelle-dev] Infinite loops with output
Aymeric Bouzy
-
2015/05/28
Re: [isabelle-dev] Cannot execute Poly/ML in 32bit mode
Makarius
-
2015/05/28
Re: [isabelle-dev] Cannot execute Poly/ML in 32bit mode
Manuel Eberl
-
2015/05/28
[isabelle-dev] Cannot execute Poly/ML in 32bit mode
Peter Lammich
-
2015/05/07
Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level
Makarius
-
2015/05/07
Re: [isabelle-dev] Folding in Isabelle/jEdit
Makarius
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Gerwin Klein
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Makarius
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Gerwin Klein
-
2015/04/28
Re: [isabelle-dev] not working
Makarius
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Makarius
-
2015/04/28
Re: [isabelle-dev] not working
Tobias Nipkow
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Tobias Nipkow
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Gerwin Klein
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Gerwin Klein
-
2015/04/28
[isabelle-dev] not working
Larry Paulson
-
2015/04/28
Re: [isabelle-dev] Status of afp-2015
Larry Paulson
-
2015/04/28
[isabelle-dev] Status of afp-2015
Makarius
-
2015/04/22
Re: [isabelle-dev] Isabelle repository broken
Makarius
-
2015/04/22
Re: [isabelle-dev] docs for new datatype package
Makarius
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Jasmin Blanchette
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Jasmin Blanchette
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Jasmin Blanchette
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Jasmin Blanchette
-
2015/04/21
Re: [isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/20
Re: [isabelle-dev] NEWS: Z3 open source
Jasmin Blanchette
-
2015/04/20
Re: [isabelle-dev] docs for new datatype package
Jasmin Blanchette
-
2015/04/20
Re: [isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/20
[isabelle-dev] APF-2015 fork
Gerwin Klein
-
2015/04/19
Re: [isabelle-dev] docs for new datatype package
Jasmin Blanchette
-
2015/04/19
Re: [isabelle-dev] Towards the Isabelle2015 release
Makarius
-
2015/04/19
Re: [isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/19
Re: [isabelle-dev] Towards the Isabelle2015 release
Makarius
-
2015/04/19
Re: [isabelle-dev] docs for new datatype package
Jasmin Blanchette
-
2015/04/19
[isabelle-dev] docs for new datatype package
Gerwin Klein
-
2015/04/18
Re: [isabelle-dev] Isabelle/jEdit hangs on exit
Makarius
-
2015/04/18
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Makarius
-
2015/04/17
Re: [isabelle-dev] Towards the Isabelle2015 release
Makarius
-
2015/04/17
Re: [isabelle-dev] NEWS: limited name space accesses
Christian Sternagel
-
2015/04/17
[isabelle-dev] AFP works
Makarius
-
2015/04/17
Re: [isabelle-dev] Fwd: [isabelle] Changing definition of finprod
Makarius
-
2015/04/17
[isabelle-dev] NEWS: isabelle build -X
Makarius
-
2015/04/17
[isabelle-dev] Fwd: [isabelle] Changing definition of finprod
Larry Paulson
-
2015/04/17
Re: [isabelle-dev] Towards the Isabelle2015 release
Makarius
-
2015/04/17
Re: [isabelle-dev] AFP still broken (AList vs. Assoc_List)
Tobias Nipkow
-
2015/04/16
Re: [isabelle-dev] Commands not in scope fail to cause errors
Makarius
-
2015/04/16
Re: [isabelle-dev] NEWS: limited name space accesses
Makarius
-
2015/04/16
[isabelle-dev] AFP still broken (AList vs. Assoc_List)
Makarius
-
2015/04/15
Re: [isabelle-dev] New proof method "rewrite"
Lars Noschinski
-
2015/04/15
Re: [isabelle-dev] NEWS: Z3 open source
Larry Paulson
-
2015/04/15
Re: [isabelle-dev] NEWS: Z3 open source
Gerwin Klein
-
2015/04/14
Re: [isabelle-dev] NEWS: Z3 open source
Makarius
-
2015/04/14
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Florian Haftmann
-
2015/04/14
Re: [isabelle-dev] NEWS: powr
Larry Paulson
-
2015/04/14
Re: [isabelle-dev] NEWS: powr
Makarius
-
2015/04/14
Re: [isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore
Makarius
-
2015/04/14
Re: [isabelle-dev] New proof method "rewrite"
Lars Noschinski
-
2015/04/14
Re: [isabelle-dev] New proof method "rewrite"
Makarius
-
2015/04/14
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Andreas Lochbihler
-
2015/04/14
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Dmitriy Traytel
-
2015/04/13
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Andreas Lochbihler
-
2015/04/13
Re: [isabelle-dev] Mira still alive?
Lars Hupel
-
2015/04/13
Re: [isabelle-dev] Isabelle repository broken
Johannes Hölzl
-
2015/04/13
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Dmitriy Traytel
-
2015/04/13
[isabelle-dev] Isabelle repository broken
Makarius
-
2015/04/12
Re: [isabelle-dev] NEWS: powr
Larry Paulson
-
2015/04/12
Re: [isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore
Florian Haftmann
-
2015/04/12
Re: [isabelle-dev] Mira still alive?
Florian Haftmann
-
2015/04/12
Re: [isabelle-dev] NEWS: powr
Florian Haftmann
-
2015/04/12
Re: [isabelle-dev] NEWS: powr
Larry Paulson
-
2015/04/12
Re: [isabelle-dev] NEWS: powr
Manuel Eberl
-
2015/04/12
[isabelle-dev] NEWS: powr
Larry Paulson
-
2015/04/10
[isabelle-dev] Isabelle/jEdit hangs on exit
Lars Noschinski
-
2015/04/09
[isabelle-dev] Towards the Isabelle2015 release
Makarius
-
2015/04/09
Re: [isabelle-dev] NEWS: Z3 open source
Jasmin Blanchette
-
2015/04/09
[isabelle-dev] NEWS: restricted name space accesses
Makarius
-
2015/04/09
Re: [isabelle-dev] NEWS: Z3 open source
Makarius
-
2015/04/09
Re: [isabelle-dev] New proof method "rewrite"
Makarius
-
2015/04/09
Re: [isabelle-dev] New proof method "rewrite"
Lars Noschinski
-
2015/04/09
Re: [isabelle-dev] NEWS: limited name space accesses
Makarius
-
2015/04/09
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Andreas Lochbihler
-
2015/04/09
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Dmitriy Traytel
-
2015/04/09
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Jasmin Blanchette
-
2015/04/09
[isabelle-dev] datatype takes minutes, but timing panel shows 10s
Andreas Lochbihler
-
2015/04/08
[isabelle-dev] NEWS: Z3 open source
Jasmin Blanchette
-
2015/04/08
Re: [isabelle-dev] Multiset insert
Florian Haftmann
-
2015/04/08
Re: [isabelle-dev] Mira still alive?
Lars Noschinski
-
2015/04/08
Re: [isabelle-dev] Multiset insert
Larry Paulson
-
2015/04/08
[isabelle-dev] Multiset insert
Tobias Nipkow
-
2015/04/07
Re: [isabelle-dev] NEWS: limited name space accesses
Tobias Nipkow
-
2015/04/07
Re: [isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore
Dmitriy Traytel
-
2015/04/07
[isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore
Makarius
-
2015/04/07
Re: [isabelle-dev] NEWS: limited name space accesses
Makarius
-
2015/04/07
Re: [isabelle-dev] NEWS: limited name space accesses
Tobias Nipkow
-
2015/04/07
Re: [isabelle-dev] NEWS: limited name space accesses
Christian Sternagel
-
2015/04/07
[isabelle-dev] NEWS: limited name space accesses
Makarius
-
2015/04/02
Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
Makarius
-
2015/04/02
Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
Peter Lammich
-
2015/04/02
Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
Makarius
-
2015/04/02
Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
Peter Lammich
-
2015/04/01
[isabelle-dev] Mira still alive?
Makarius
-
2015/04/01
[isabelle-dev] NEWS: isabelle build -k and -x
Makarius
-
2015/04/01
[isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context
Makarius
-
2015/04/01
[isabelle-dev] NEWS: THEN_ALL_NEW in Isar method expressions
Makarius
-
2015/04/01
[isabelle-dev] NEWS: command 'experiment'
Makarius
-
2015/03/30
Re: [isabelle-dev] [isabelle] Semirings in HOL/Algebra/Ring
Johannes Hölzl
-
2015/03/29
Re: [isabelle-dev] [isabelle] Semirings in HOL/Algebra/Ring
Thiemann, Rene
-
2015/03/29
Re: [isabelle-dev] NEWS: proper Isar context for rule instantiations
Makarius
-
2015/03/29
[isabelle-dev] NEWS: proper Isar context for rule instantiations
Makarius
-
2015/03/26
Re: [isabelle-dev] Someone messed up HOL_library/Multiset_Order
Jasmin Blanchette
-
2015/03/26
[isabelle-dev] Someone messed up HOL_library/Multiset_Order
Peter Lammich
-
2015/03/26
Re: [isabelle-dev] Multiset_Order
Florian Haftmann
-
2015/03/26
Re: [isabelle-dev] Multiset_Order
Florian Haftmann
-
2015/03/25
[isabelle-dev] Suppress odd .prv files
Makarius
-
2015/03/24
Re: [isabelle-dev] Reprocessing in Isabelle/jEdit
Makarius
-
2015/03/24
Re: [isabelle-dev] Reprocessing in Isabelle/jEdit
Peter Lammich
-
2015/03/24
[isabelle-dev] Reprocessing in Isabelle/jEdit
Jasmin Blanchette
-
2015/03/23
Re: [isabelle-dev] Problem in the AFP
Thiemann, Rene
-
2015/03/23
Re: [isabelle-dev] Problem in the AFP
Peter Lammich
-
2015/03/21
Re: [isabelle-dev] Problem in the AFP
Lawrence Paulson
-
2015/03/21
Re: [isabelle-dev] Problem in the AFP
Peter Lammich
-
2015/03/21
[isabelle-dev] Problem in the AFP
Florian Haftmann
-
2015/03/20
Re: [isabelle-dev] Mira/AFP broken?
Lars Noschinski
-
2015/03/19
[isabelle-dev] Mira/AFP broken?
Makarius
-
2015/03/19
Re: [isabelle-dev] HOL-Probability broken
Makarius
-
2015/03/18
Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
Makarius
-
2015/03/18
Re: [isabelle-dev] HOL-Probability broken
Larry Paulson
-
2015/03/18
Re: [isabelle-dev] HOL-Probability broken
Makarius
-
2015/03/18
[isabelle-dev] New proof method "rewrite"
Lars Noschinski
-
2015/03/17
Re: [isabelle-dev] HOL-Probability broken
Larry Paulson
-
2015/03/17
Re: [isabelle-dev] HOL-Probability broken
Larry Paulson
-
2015/03/17
[isabelle-dev] HOL-Probability broken
Makarius
-
2015/03/16
Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
Makarius
-
2015/03/16
Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
Makarius
-
2015/03/12
Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)
Andreas Lochbihler
-
2015/03/12
Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)
Andreas Lochbihler
-
2015/03/12
Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)
Makarius
-
2015/03/05
Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
Makarius
-
2015/03/05
Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
Christian Sternagel
-
2015/03/05
[isabelle-dev] Isabelle gets stuck when imported theory is not found
Johannes Hölzl
-
2015/03/03
Re: [isabelle-dev] What is this 3 levels of lambda calculi?
Makarius
-
2015/03/02
[isabelle-dev] What is this 3 levels of lambda calculi?
Askar Safin
-
2015/02/19
Re: [isabelle-dev] Regression in the sublocale command
Clemens Ballarin
-
2015/02/17
Re: [isabelle-dev] Improved Graphview
Lars Noschinski
-
2015/02/17
Re: [isabelle-dev] [isabelle] Code generator produces non-linear patterns
Florian Haftmann
-
2015/02/17
Re: [isabelle-dev] Regression in the sublocale command
Florian Haftmann
-
2015/02/16
Re: [isabelle-dev] Constructors and the predicate compiler
Andreas Lochbihler
-
2015/02/16
[isabelle-dev] Consturctors and the predicate compiler
Florian Haftmann
-
2015/02/15
Re: [isabelle-dev] sign_simps
Florian Haftmann
-
2015/02/15
Re: [isabelle-dev] sign_simps
Tobias Nipkow
-
2015/02/15
Re: [isabelle-dev] Regression in the sublocale command
Clemens Ballarin
-
2015/02/15
Re: [isabelle-dev] sign_simps
Florian Haftmann
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Clemens Ballarin
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Florian Haftmann
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Florian Haftmann
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Florian Haftmann
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Florian Haftmann
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Florian Haftmann
-
2015/02/14
Re: [isabelle-dev] sign_simps
Larry Paulson
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Clemens Ballarin
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Clemens Ballarin
-
2015/02/14
Re: [isabelle-dev] Regression in the sublocale command
Florian Haftmann
-
2015/02/14
[isabelle-dev] sign_simps
Florian Haftmann
-
2015/02/14
[isabelle-dev] Constructors and the predicate compiler
Florian Haftmann