cl-isabelle-users@lists.cam.ac.uk

0

replies

[Isabelle] Re: Quantum Computing

started 2018-09-07 09:27:19 UTC

2018-09-07 09:27:19 UTC

José Manuel Rodriguez Caballero

2

replies

Possible bug in Finite_Map

started 2018-09-05 15:10:51 UTC

2018-09-06 11:21:54 UTC

Andreas Lochbihler

4

replies

Concurrent/counter.ML

started 2018-09-04 05:26:48 UTC

2018-09-05 17:21:01 UTC

Makarius

2

replies

Can the empty relation be inductive?

started 2018-09-05 01:00:28 UTC

2018-09-05 01:22:10 UTC

Ching-Tsun Chou

12

replies

Intel Core i9

started 2018-08-20 17:20:15 UTC

2018-09-05 01:03:03 UTC

Ching-Tsun Chou

0

replies

New in the AFP: The Budan-Fourier Theorem and Counting Real Roots with Multiplicity

started 2018-09-04 19:02:36 UTC

2018-09-04 19:02:36 UTC

Thiemann, René

2

replies

How do I prove "¬ 2 ≤ 1" and use a simple lemma?

started 2018-09-04 12:11:53 UTC

2018-09-04 12:29:42 UTC

Ching-Tsun Chou

6

replies

How do I prove "foo 2 = foo (Suc (Suc 0))"?

started 2018-09-04 02:34:22 UTC

2018-09-04 10:53:38 UTC

Tobias Nipkow

0

replies

Question about simp

started 2018-09-04 04:43:56 UTC

2018-09-04 04:43:56 UTC

Ching-Tsun Chou

2

replies

refl can be proved

started 2018-09-02 22:24:52 UTC

2018-09-03 17:36:09 UTC

Christian Sternagel

0

replies

"undefined" can be defined :)

started 2018-09-02 21:11:25 UTC

2018-09-02 21:11:25 UTC

Elsa L. Gunter

0

replies

Problem sledgehammer/presburger

started 2018-09-01 17:46:37 UTC

2018-09-01 17:46:37 UTC

Jørgen Villadsen

0

replies

Zohar Manna is no longer with us

started 2018-08-30 18:58:39 UTC

2018-08-30 18:58:39 UTC

Nachum Dershowitz

2

replies

Proving implication (a --> c) from (b --> c) given relation between a and b

started 2018-08-30 14:26:22 UTC

2018-08-30 14:37:17 UTC

Manuel Eberl

2

replies

map totality

started 2018-08-28 18:34:34 UTC

2018-08-29 19:06:34 UTC

Lars Hupel

1

reply

The Arithmetic Site in Isabelle/CTT (was: Isabelle/HoTT)

started 2018-08-28 09:06:49 UTC

2018-08-29 17:41:35 UTC

Lawrence Paulson

0

replies

CfP: Symposium on Practical Aspects of Declarative Languages (PADL-2019)

started 2018-08-29 17:21:46 UTC

2018-08-29 17:21:46 UTC

Moa Johansson

9

replies

Issues of Isabelle

started 2018-08-15 14:28:06 UTC

2018-08-29 13:16:33 UTC

Chun Tian (binghe)

0

replies

[ACL2-2018] Call for Participation --- Registration Open!

started 2018-08-28 23:44:46 UTC

2018-08-28 23:44:46 UTC

Alessandro Coglio

2

replies

Checksum and Decryption in HOL/Auth library using Inductive Method

started 2018-08-21 14:22:06 UTC

2018-08-28 19:09:14 UTC

Lawrence Paulson

2

replies

Duplicate theory name: Draft.KEStore, Isac.KEStore

started 2018-08-27 20:27:30 UTC

2018-08-28 16:43:42 UTC

Walther Neuper

0

replies

Final Call for Papers Software Verification and Testing Track (SVT) @ ACM SAC 2019

started 2018-08-28 13:37:53 UTC

2018-08-28 13:37:53 UTC

Matthias Güdemann

2

replies

Help with using AFP from Isabelle on Windows

started 2018-08-22 15:02:37 UTC

2018-08-28 01:03:41 UTC

Makarius

7

replies

adjacent facets

started 2018-08-24 20:09:18 UTC

2018-08-27 09:44:46 UTC

José Manuel Rodriguez Caballero

0

replies

new in the AFP: Simplex

started 2018-08-27 09:30:31 UTC

2018-08-27 09:30:31 UTC

Gerwin Klein

1

reply

\<^locale> antiquotation does not work

started 2018-08-22 23:43:48 UTC

2018-08-26 14:11:14 UTC

Makarius

1

reply

missing *.thy files for published papers

started 2018-08-26 07:50:46 UTC

2018-08-26 12:50:04 UTC

Tobias Nipkow

0

replies

applications of Minsky Machines to number theory

started 2018-08-25 08:26:11 UTC

2018-08-25 08:26:11 UTC

José Manuel Rodriguez Caballero

4

replies

Isabelle documentation – Re: Help with Triangulation

started 2018-08-20 04:53:47 UTC

2018-08-24 17:18:09 UTC

Tobias Nipkow

4

replies

metis -unused theorems

started 2018-08-22 04:20:10 UTC

2018-08-23 16:07:39 UTC

Dominique Unruh