August 2013 Archives by thread

• Messages sorted by: [ subject ] [ author ] [ date ]
• More info on this list...

Starting: Thu Aug 1 16:41:18 CEST 2013
Ending: Sat Aug 31 13:02:38 CEST 2013
Messages: 104

• [isabelle-dev] isabelle dimacs2hol   Makarius
  • [isabelle-dev] isabelle dimacs2hol   Tjark Weber
• [isabelle-dev] type unification   Makarius
• [isabelle-dev] adhoc overloading   Makarius
  • [isabelle-dev] adhoc overloading   Christian Sternagel
    • [isabelle-dev] adhoc overloading   Makarius
      • [isabelle-dev] adhoc overloading   Christian Sternagel
      • [isabelle-dev] adhoc overloading   Makarius
• [isabelle-dev] lemma addition   Makarius
  • [isabelle-dev] lemma addition   Lars Noschinski
• [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Makarius
  • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Jasmin Blanchette
    • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Florian Haftmann
      • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Andreas Schropp
      • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Jasmin Blanchette
  • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Florian Haftmann
    • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Dmitriy Traytel
      • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Florian Haftmann
      • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Christian Urban
      • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Andreas Lochbihler
      • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Christian Urban
    • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Jasmin Blanchette
  • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Alexander Krauss
    • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Jasmin Blanchette
      • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Alexander Krauss
  • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Andrei Popescu
  • [isabelle-dev] New (Co)datatypes: Status & Plan (FYI)   Andrei Popescu
• [isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style   Florian Haftmann
• [isabelle-dev] some actual find_theorems functionality (fb1f026c48ff)   Fabian Immler
  • [isabelle-dev] some actual find_theorems functionality (fb1f026c48ff)   Makarius
    • [isabelle-dev] some actual find_theorems functionality (fb1f026c48ff)   Fabian Immler
• [isabelle-dev] partial_function   Christian Sternagel
  • [isabelle-dev] partial_function   Christian Sternagel
    • [isabelle-dev] partial_function   Makarius
• [isabelle-dev] Mixfix-Syntax not recognized   René Neumann
  • [isabelle-dev] Mixfix-Syntax not recognized   René Neumann
  • [isabelle-dev] Mixfix-Syntax not recognized   René Neumann
  • [isabelle-dev] Mixfix-Syntax not recognized   Makarius
• [isabelle-dev] Sum_of_Squares_Remote failure   Makarius
  • [isabelle-dev] Sum_of_Squares_Remote failure   Gerwin Klein
    • [isabelle-dev] Sum_of_Squares_Remote failure   Makarius
      • [isabelle-dev] Sum_of_Squares_Remote failure   Tobias Nipkow
• [isabelle-dev] Subscripts within identifiers   Makarius
  • [isabelle-dev] Subscripts within identifiers   Gerwin Klein
• [isabelle-dev] NEWS: Dockable window "Find"   Makarius
  • [isabelle-dev] NEWS: Dockable window "Find"   Gerwin Klein
    • [isabelle-dev] NEWS: Dockable window "Find"   Makarius
      • [isabelle-dev] NEWS: Dockable window "Find"   Gerwin Klein
      • [isabelle-dev] NEWS: Dockable window "Find"   Gerwin Klein
      • [isabelle-dev] NEWS: Dockable window "Find"   Gerwin Klein
• [isabelle-dev] Problems with Code-Generator   René Thiemann
  • [isabelle-dev] Problems with Code-Generator   Andreas Lochbihler
    • [isabelle-dev] Problems with Code-Generator   René Thiemann
      • [isabelle-dev] Problems with Code-Generator   Andreas Lochbihler
      • [isabelle-dev] Problems with Code-Generator   Florian Haftmann
      • [isabelle-dev] Problems with Code-Generator   René Thiemann
• [isabelle-dev] including raises Attempt to perform non-trivial merge of theories   Andreas Lochbihler
  • [isabelle-dev] including raises Attempt to perform non-trivial merge of theories   Ondřej Kunčar
    • [isabelle-dev] including raises Attempt to perform non-trivial merge of theories   Makarius
      • [isabelle-dev] including raises Attempt to perform non-trivial merge of theories   Makarius
• [isabelle-dev] problem with the proof recording   Ondřej Kunčar
• [isabelle-dev] NEWS: Simplified subscripts within identifiers   Makarius
• [isabelle-dev] string and altstring   Christian Sternagel
• [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Lawrence Paulson
  • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Makarius
    • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Lawrence Paulson
    • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Lars Noschinski
      • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Makarius
    • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Tobias Nipkow
      • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Lawrence Paulson
      • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Tobias Nipkow
      • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Lawrence Paulson
      • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Makarius
      • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Lawrence Paulson
      • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Makarius
  • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Makarius
    • [isabelle-dev] [isabelle] match_tac, schematic and bound variables   Tobias Nipkow
• [isabelle-dev] isabelle doc functions   Christian Sternagel
  • [isabelle-dev] isabelle doc functions   Makarius
    • [isabelle-dev] isabelle doc functions   Alexander Krauss
• [isabelle-dev] NEWS: sledgehammer panel   Makarius
• [isabelle-dev] The coming release   Makarius
  • [isabelle-dev] The coming release   Florian Haftmann
  • [isabelle-dev] The coming release   Alexander Krauss
• [isabelle-dev] Draft toy for proof exploration   Florian Haftmann
  • [isabelle-dev] Draft toy for proof exploration   Dmitriy Traytel
• [isabelle-dev] Monad_Syntax   Christian Sternagel
  • [isabelle-dev] Monad_Syntax   Alexander Krauss
• [isabelle-dev] functions over abstract data   Christian Sternagel
  • [isabelle-dev] functions over abstract data   Alexander Krauss
• [isabelle-dev] print_theorems uses a wrong context?   Ondřej Kunčar
• [isabelle-dev] support for ideas using isabelle hol   David Blubaugh
  • [isabelle-dev] support for ideas using isabelle hol   Lawrence Paulson
• [isabelle-dev] numpad doesn't work   Ondřej Kunčar
  • [isabelle-dev] numpad doesn't work   Makarius
    • [isabelle-dev] numpad doesn't work   Ondřej Kunčar
      • [isabelle-dev] numpad doesn't work   Makarius
• [isabelle-dev] NEWS: Improved completion mechanism   Makarius
  • [isabelle-dev] NEWS: Improved completion mechanism   Christian Sternagel
• [isabelle-dev] Popups in Java/Swing   Makarius
• [isabelle-dev] jEdit: re-checking of main buffer   Christian Sternagel
• [isabelle-dev] sledgehammer response   Tobias Nipkow
• [isabelle-dev] sledgehammer   Tobias Nipkow
  • [isabelle-dev] sledgehammer   Lawrence Paulson

Last message date: Sat Aug 31 13:02:38 CEST 2013
Archived on: Fri Apr 12 08:42:18 CEST 2019

• Messages sorted by: [ subject ] [ author ] [ date ]
• More info on this list...