Jean-Christophe Filliâtre 53b3249062 list.Distinct using a recursive definition

2025-05-14 17:32:28 +02:00

..

etc

clarified jEdit server mode: start "isabelle why3_jedit" first and let why3ide connect to via "isabelle why3 -i jedit"

2014-01-28 17:06:51 +01:00

Tools

Implemented client for processing jobs using Isabelle server

2018-08-20 14:05:43 +02:00

realizations

list.Distinct using a recursive definition

2025-05-14 17:32:28 +02:00

ROOT.2019

Adapt to Isabelle2021-1

2022-03-24 12:11:12 +01:00

ROOT.2021-1

Adapt to Isabelle2021-1

2022-03-24 12:11:12 +01:00

why3.ML.2019

Fix conjunctions in Isabelle (fix #491).

2021-06-11 16:49:05 +02:00

why3.ML.2021-1

Fix conjunctions in Isabelle (fix #491).

2023-01-16 10:04:12 +01:00

Why3_Bool.thy

Add support for Isabelle 2022.

2023-02-24 18:46:25 +01:00

Why3_BV.thy.2019

Adapted to Isabelle2019

2020-03-03 09:58:48 +01:00

Why3_BV.thy.2021-1

Adapt to Isabelle2021-1

2022-03-24 12:11:12 +01:00

Why3_Int.thy

Add support for Isabelle 2022.

2023-02-24 18:46:25 +01:00

Why3_List.thy

Add support for Isabelle 2022.

2023-02-24 18:46:25 +01:00

Why3_Map.thy.2019

Add support for Isabelle 2022.

2023-02-24 18:46:25 +01:00

Why3_Map.thy.2021-1

Add support for Isabelle 2022.

2023-02-24 18:46:25 +01:00

Why3_Number.thy

Add support for Isabelle 2022.

2023-02-24 18:46:25 +01:00

Why3_Real.thy

add isabelle proofs for new axioms and lemmas in real.ExpLog

2024-04-17 14:22:39 +02:00

Why3_Set.thy

fix realizations

2024-11-13 19:10:42 +01:00

Why3_Setup.thy

Provided Isabelle realization of bit vector theory

2015-09-28 17:08:18 +02:00

Why3.thy

Changed the unsecure trusted_wf attribute mechanism into a more secure one

2023-02-22 13:50:29 +00:00