Cl-isabelle-users September 2012 Archives by author

• September 2012 messages sorted by: [ thread ] [ subject ] [ date ]
• More info on this list...
• List archive Table of Contents

• 後藤　裕貴, auf75646@kwansei.ac.jp
  • [isabelle] "distinct" for Datatype - Sun, 16 Sep 2012 20:42:40 +0100
• René Thiemann, rene.thiemann@uibk.ac.at
  • Re: [isabelle] substitution - Wed, 12 Sep 2012 14:21:00 +0100
  • Re: [isabelle] substitution - Wed, 12 Sep 2012 14:34:57 +0100
• René Neumann, rene.neumann@in.tum.de
  • [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Wed, 05 Sep 2012 12:43:11 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Wed, 05 Sep 2012 14:49:35 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Wed, 05 Sep 2012 15:23:50 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Tue, 18 Sep 2012 06:25:38 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Wed, 19 Sep 2012 14:30:30 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Thu, 20 Sep 2012 09:19:03 +0100
• René Neumann, rene.neumann@in.tum.de
  • Re: [isabelle] Emacs hurts - Tue, 04 Sep 2012 11:26:55 +0100
  • Re: [isabelle] Strong Induction - Sat, 08 Sep 2012 23:37:46 +0100
• Aaron W . Hsu, arcfide@sacrideo.us
  • [isabelle] Dealing with Int and Nat at the same time - Sat, 01 Sep 2012 01:55:24 +0100
  • [isabelle] Dealing with functions - Thu, 06 Sep 2012 00:14:03 +0100
  • Re: [isabelle] Dealing with functions - Thu, 06 Sep 2012 13:06:18 +0100
• Alfio Martini, alfio.martini@acm.org
  • Re: [isabelle] Strong Induction - Sat, 08 Sep 2012 21:10:59 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Tue, 11 Sep 2012 23:26:16 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 18:30:36 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 18:35:47 +0100
  • Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances) - Sat, 15 Sep 2012 00:13:40 +0100
  • Re: [isabelle] Eliminating two quantifiers in structural proof - Sun, 16 Sep 2012 12:04:35 +0100
  • Re: [isabelle] Eliminating two quantifiers in structural proof - Sun, 16 Sep 2012 12:15:11 +0100
  • Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances) - Sun, 16 Sep 2012 16:00:28 +0100
• Andreas Lochbihler, andreas.lochbihler@kit.edu
  • Re: [isabelle] Wellsortedness error by using user defined function in quickcheck - Mon, 03 Sep 2012 09:54:03 +0100
  • Re: [isabelle] Wellsortedness error by using user defined function in quickcheck - Wed, 19 Sep 2012 07:34:13 +0100
• Brian Huffman, huffman@in.tum.de
  • Re: [isabelle] A simple lemma - Fri, 07 Sep 2012 17:37:16 +0100
• Clemens Ballarin, ballarin@in.tum.de
  • [isabelle] Polynomial Theories - Thu, 06 Sep 2012 20:22:40 +0100
• David Greenaway, david.greenaway@nicta.com.au
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Fri, 14 Sep 2012 01:11:25 +0100
• David Matthews, dm@prolingua.co.uk
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Thu, 13 Sep 2012 13:23:26 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 17 Sep 2012 12:08:45 +0100
• Dmitriy Traytel, traytel@in.tum.de
  • Re: [isabelle] COERCION_GEN_ERROR ? - Tue, 04 Sep 2012 19:58:55 +0100
  • Re: [isabelle] COERCION_GEN_ERROR ? - Wed, 05 Sep 2012 09:55:58 +0100
  • [isabelle] Code generation for sorts from locales - Sat, 15 Sep 2012 21:16:45 +0100
  • Re: [isabelle] Code generation for sorts from locales - Sun, 16 Sep 2012 17:17:58 +0100
• Edward Schwartz, edmcman@cmu.edu
  • [isabelle] Creating fresh logical variables - Tue, 11 Sep 2012 19:09:01 +0100
  • [isabelle] Eliminating two quantifiers in structural proof - Sat, 15 Sep 2012 21:15:27 +0100
  • Re: [isabelle] Eliminating two quantifiers in structural proof - Sat, 15 Sep 2012 22:51:12 +0100
• Elsa L Gunter, egunter@illinois.edu
  • Re: [isabelle] Defining equality for a new type - Fri, 07 Sep 2012 16:51:21 +0100
• Felipe Magno de Almeida, felipe.m.almeida@gmail.com
  • [isabelle] Strong Induction - Sat, 08 Sep 2012 18:49:39 +0100
• Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] Code generation for sorts from locales - Sun, 16 Sep 2012 16:34:17 +0100
  • [isabelle] Type and sort annotations in jEdit - Sat, 22 Sep 2012 19:44:31 +0100
  • Re: [isabelle] Code generation for sorts from locales - Sat, 22 Sep 2012 21:55:09 +0100
  • Re: [isabelle] Missing codegen theory - Sat, 29 Sep 2012 07:07:38 +0100
• Gerwin Klein, gerwin.klein@nicta.com.au
  • Re: [isabelle] Simpl in AFP release for 2011-1 does not build - Thu, 06 Sep 2012 00:36:59 +0100
  • Re: [isabelle] Simpl in AFP release for 2011-1 does not build - Thu, 06 Sep 2012 01:09:12 +0100
  • [isabelle] Last Call for Papers: Systems Software Verification SSV 2012, Sydney. Nov 28-30, 2012 - Tue, 11 Sep 2012 12:11:09 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Thu, 13 Sep 2012 14:34:29 +0100
  • [isabelle] deadline extension: Systems Software Verification (SSV'12) - Thu, 20 Sep 2012 13:03:28 +0100
• Gopalan Nadathur, gopalan@cs.umn.edu
  • [isabelle] Book Announcement - Fri, 07 Sep 2012 21:38:13 +0100
• Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] Mere synonyms or the properties of equality being used? - Mon, 03 Sep 2012 18:25:07 +0100
  • Re: [isabelle] Mere synonyms or the properties of equality being used? - Mon, 03 Sep 2012 20:57:51 +0100
  • [isabelle] Minimizer and preplay - 2 of the many amazing features of Sledgehammer - Tue, 04 Sep 2012 17:55:12 +0100
  • [isabelle] Sledge and 0; green & blue; ATPs lovin' quantifiers - Fri, 07 Sep 2012 00:52:19 +0100
  • Re: [isabelle] Sledge and 0; green & blue; ATPs lovin' quantifiers - Fri, 07 Sep 2012 01:26:15 +0100
  • [isabelle] Isar feature request: bbold and ebold - Mon, 10 Sep 2012 18:08:31 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Tue, 11 Sep 2012 13:20:40 +0100
  • [isabelle] Thanks Nitpick for actually answering a former, simple question - Tue, 11 Sep 2012 21:07:49 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 17:06:35 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 17:40:06 +0100
  • Re: [isabelle] Isar feature request: bbold and ebold - Wed, 12 Sep 2012 20:18:35 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 20:42:18 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 20:50:41 +0100
  • Re: [isabelle] Isar feature request: bbold and ebold - Wed, 12 Sep 2012 21:10:41 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Wed, 12 Sep 2012 21:15:51 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Thu, 13 Sep 2012 19:12:36 +0100
  • [isabelle] Free variables aren't quantified, it's that simple (by all appearances) - Fri, 14 Sep 2012 05:52:40 +0100
  • Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances) - Fri, 14 Sep 2012 14:29:45 +0100
  • Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances) - Sat, 15 Sep 2012 04:30:49 +0100
  • Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances) - Sat, 15 Sep 2012 05:18:18 +0100
  • Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances) - Mon, 17 Sep 2012 17:35:42 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Mon, 17 Sep 2012 19:35:33 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Sun, 23 Sep 2012 17:46:18 +0100
• Henri . Debrat, Henri.Debrat@loria.fr
  • [isabelle] exception Option - Wed, 05 Sep 2012 13:16:24 +0100
• Holger Blasum, hbl@sysgo.com
  • [isabelle] Range of a record-valued function - Wed, 26 Sep 2012 10:09:21 +0100
• Jasmin Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] Dealing with Int and Nat at the same time - Sun, 02 Sep 2012 19:52:04 +0100
  • Re: [isabelle] Insufficient memory when building heap image - Fri, 28 Sep 2012 16:29:01 +0100
• Johannes Hölzl, hoelzl@in.tum.de
  • Re: [isabelle] Comparing two graphs - Wed, 12 Sep 2012 18:05:11 +0100
  • Re: [isabelle] Comparing pairs - Fri, 14 Sep 2012 06:54:09 +0100
• John Munroe, munddr@gmail.com
  • [isabelle] Defining equality for a new type - Fri, 07 Sep 2012 16:20:06 +0100
  • [isabelle] A simple lemma - Fri, 07 Sep 2012 17:25:54 +0100
  • [isabelle] Comparing two graphs - Wed, 12 Sep 2012 17:38:28 +0100
  • Re: [isabelle] Comparing two graphs - Wed, 12 Sep 2012 22:33:35 +0100
  • [isabelle] Comparing pairs - Thu, 13 Sep 2012 23:29:51 +0100
  • [isabelle] A simple lemma? - Fri, 14 Sep 2012 01:12:48 +0100
• John Wickerson, jpw48@cam.ac.uk
  • Re: [isabelle] Defining equality for a new type - Fri, 07 Sep 2012 16:24:28 +0100
  • Re: [isabelle] Defining equality for a new type - Fri, 07 Sep 2012 16:26:18 +0100
• Lars Noschinski, noschinl@in.tum.de
  • [isabelle] Simpl in AFP release for 2011-1 does not build - Wed, 05 Sep 2012 10:40:17 +0100
  • Re: [isabelle] Simpl in AFP release for 2011-1 does not build - Wed, 05 Sep 2012 11:25:55 +0100
  • Re: [isabelle] exception Option - Wed, 05 Sep 2012 13:49:53 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Tue, 11 Sep 2012 21:52:31 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Tue, 11 Sep 2012 22:00:42 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Thu, 13 Sep 2012 10:56:55 +0100
• Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Product types? - Mon, 03 Sep 2012 10:47:47 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Tue, 11 Sep 2012 21:55:47 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 14:47:19 +0100
• Lukas Bulwahn, bulwahn@in.tum.de
  • Re: [isabelle] Wellsortedness error by using user defined function in quickcheck - Mon, 03 Sep 2012 10:09:15 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 17 Sep 2012 08:51:51 +0100
• Makarius, makarius@sketis.net
  • Re: [isabelle] Naive question about tactics and Pure - Mon, 03 Sep 2012 09:26:47 +0100
  • Re: [isabelle] Proofmanagement - Mon, 03 Sep 2012 09:36:25 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Wed, 05 Sep 2012 14:42:09 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Wed, 12 Sep 2012 19:16:34 +0100
  • Re: [isabelle] Isar feature request: bbold and ebold - Wed, 12 Sep 2012 19:34:42 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Wed, 12 Sep 2012 19:43:06 +0100
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Wed, 12 Sep 2012 19:55:05 +0100
  • Re: [isabelle] Isar feature request: bbold and ebold - Wed, 12 Sep 2012 20:43:17 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Wed, 12 Sep 2012 21:31:00 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Wed, 12 Sep 2012 22:49:39 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Thu, 13 Sep 2012 15:40:19 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Thu, 13 Sep 2012 15:47:27 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Sun, 16 Sep 2012 19:54:34 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Sun, 16 Sep 2012 20:04:32 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 17 Sep 2012 10:47:58 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 17 Sep 2012 12:40:52 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 17 Sep 2012 13:46:59 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Mon, 17 Sep 2012 14:31:27 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Wed, 19 Sep 2012 13:41:42 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Wed, 19 Sep 2012 14:49:37 +0100
  • Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround) - Fri, 21 Sep 2012 11:03:19 +0100
  • Re: [isabelle] Isar feature request: bbold ... (& italics, ibold) - Fri, 21 Sep 2012 19:15:55 +0100
  • Re: [isabelle] Type and sort annotations in jEdit - Sat, 22 Sep 2012 20:02:31 +0100
  • Re: [isabelle] Type and sort annotations in jEdit - Sat, 22 Sep 2012 20:09:14 +0100
  • Re: [isabelle] Eliminating two quantifiers in structural proof - Mon, 24 Sep 2012 20:52:20 +0100
  • Re: [isabelle] Eliminating two quantifiers in structural proof - Mon, 24 Sep 2012 20:59:34 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 24 Sep 2012 21:11:52 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 24 Sep 2012 21:23:41 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Wed, 26 Sep 2012 14:55:12 +0100
  • Re: [isabelle] Insufficient memory when building heap image - Fri, 28 Sep 2012 15:45:20 +0100
• Manuel Eberl, eberlm@in.tum.de
  • [isabelle] Unicode Tokens constantly switched off in Proof General - Tue, 18 Sep 2012 01:29:21 +0100
  • [isabelle] Insufficient memory when building heap image - Fri, 28 Sep 2012 14:47:18 +0100
  • Re: [isabelle] Insufficient memory when building heap image - Fri, 28 Sep 2012 15:54:18 +0100
  • Re: [isabelle] Insufficient memory when building heap image - Sat, 29 Sep 2012 16:07:06 +0100
• Matthew Fernandez, matthew.fernandez@nicta.com.au
  • [isabelle] Missing codegen theory - Fri, 28 Sep 2012 13:32:00 +0100
• Peter Lammich, lammich@in.tum.de
  • [isabelle] COERCION_GEN_ERROR ? - Tue, 04 Sep 2012 18:24:42 +0100
• Prathamesh, prathamesh.t@gmail.com
  • [isabelle] substitution - Tue, 11 Sep 2012 13:12:19 +0100
  • Re: [isabelle] substitution - Wed, 12 Sep 2012 13:38:30 +0100
  • Re: [isabelle] substitution - Wed, 12 Sep 2012 13:38:35 +0100
• Rafal Kolanski, xs@xaph.net
  • Re: [isabelle] Emacs hurts - Sun, 02 Sep 2012 13:38:02 +0100
  • [isabelle] Parallel proofs issue, potentially in subst method - Mon, 10 Sep 2012 07:27:51 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method - Thu, 13 Sep 2012 02:34:40 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Thu, 13 Sep 2012 23:58:39 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Fri, 14 Sep 2012 05:55:38 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Sun, 16 Sep 2012 23:39:35 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Mon, 17 Sep 2012 12:22:06 +0100
  • Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces) - Tue, 25 Sep 2012 08:46:53 +0100
• Ramana Kumar, rk436@cam.ac.uk
  • Re: [isabelle] Mere synonyms or the properties of equality being used? - Mon, 03 Sep 2012 19:18:45 +0100
• Thomas Sewell, Thomas.Sewell@nicta.com.au
  • Re: [isabelle] Range of a record-valued function - Thu, 27 Sep 2012 04:44:01 +0100
• Tim (McKenzie) Makarios, tjm1983@gmail.com
  • Re: [isabelle] rigorous axiomatic geometry proof in Isabelle - Fri, 14 Sep 2012 00:48:15 +0100
  • Re: [isabelle] rigorous axiomatic geometry proof in Isabelle - Fri, 14 Sep 2012 00:52:30 +0100
• Tjark Weber, webertj@in.tum.de
  • Re: [isabelle] Thanks Nitpick for actually answering a former, simple question - Tue, 11 Sep 2012 22:17:50 +0100
  • Re: [isabelle] Range of a record-valued function - Thu, 27 Sep 2012 08:01:24 +0100
• Tobias Nipkow, nipkow@in.tum.de
  • Re: [isabelle] Dealing with functions - Thu, 06 Sep 2012 00:47:46 +0100
  • Re: [isabelle] Dealing with functions - Mon, 10 Sep 2012 01:16:26 +0100
  • Re: [isabelle] Strong Induction - Mon, 10 Sep 2012 01:52:42 +0100
  • [isabelle] New AFP entry: Possibilistic Noninterference - Mon, 10 Sep 2012 07:21:26 +0100
  • Re: [isabelle] Eliminating two quantifiers in structural proof - Sat, 15 Sep 2012 23:35:50 +0100
• Viorel Preoteasa, viorel.preoteasa@abo.fi
  • Re: [isabelle] A simple lemma - Fri, 07 Sep 2012 17:39:16 +0100
• Walther Neuper, wneuper@ist.tugraz.at
  • [isabelle] eduTPS Sept.22 deadline extension - Sat, 15 Sep 2012 08:59:16 +0100
• Yuhui Lin, Y.H.Lin-2@sms.ed.ac.uk
  • Re: [isabelle] Wellsortedness error by using user defined function in quickcheck - Mon, 03 Sep 2012 09:39:32 +0100
  • Re: [isabelle] Wellsortedness error by using user defined function in quickcheck - Tue, 18 Sep 2012 16:34:36 +0100