diff --git a/docs/index.md b/docs/index.md index f890a1a..daab862 100644 --- a/docs/index.md +++ b/docs/index.md @@ -3,14 +3,14 @@ This web page contains information for users and developers of the KeY Deductive Verification System. -If you are new to the KeY System, you should start with the excerpt [Using the Prover](user/quicktour/) from the KeY Book. +If you are new to the KeY System, you should start with the excerpt [Using the Prover](quicktour/) from the KeY Book. The documentation is split into two major parts: * End user: - * [How to use the KeY tool for *end user*](user/) - * [How to write Proof Scripts for resilient, persistent and reapplicable proofs*](workbench/Proof Scripts/) + * [How to use the KeY tool for *end user*](user/FAQ.md) + * [How to write Proof Scripts for resilient, persistent and reapplicable proofs*](workbench/Proof%20Scripts/) * Developer: * [How to use KeY as a library or add a new feature](devel/) * [How we test KeY](devel/Testing/) diff --git a/docs/user/IsabelleTranslation/index.md b/docs/user/IsabelleTranslation/index.md index 6a6a2d6..9c211ff 100644 --- a/docs/user/IsabelleTranslation/index.md +++ b/docs/user/IsabelleTranslation/index.md @@ -4,8 +4,8 @@ !!! abstract - This note describes the new *Isabelle Translation* extension in KeY 2.12.3 - When enabled it can be used to translate sequents to Isabelle and automatically search for proofs using Isabelle + This note describes the new *Isabelle Translation* extension in KeY 2.12.4 + When enabled it can be used to translate sequents to Isabelle and automatically search for proofs using Isabelle ## Overview @@ -42,7 +42,7 @@ To use the automatic proof search parts of the Isabelle Translation, an Isabelle ## Settings -Currently the Isabelle Translation provides two settings. These are found under Options>Settings>Isabelle Translation. +Currently the Isabelle Translation provides three settings. These are found under Options>Settings>Isabelle Translation. `Location for translation files` >This setting determines where the translation files should be stored. This includes the session files as well as the Isabelle theories for the preamble and the sequent translation. @@ -53,7 +53,7 @@ Currently the Isabelle Translation provides two settings. These are found under `Timeout` >This setting sets the timeout for proof searches in seconds. -There is an additional button to check if a given version of Isabelle is supported. Currently the supported versions are Isabelle2023 and Isabelle2024-RC1. +There is an additional button to check if a given version of Isabelle is supported. The currently supported versions are Isabelle2023, Isabelle2024, Isabelle2025. ## Translation Structure diff --git a/docs/user/UiFeatures/index.md b/docs/user/UiFeatures/index.md index d70a409..017e0b2 100644 --- a/docs/user/UiFeatures/index.md +++ b/docs/user/UiFeatures/index.md @@ -2,4 +2,5 @@ - [Node Differences](../NodeDiff) - [Proof Slicing](../ProofSlicing) - [Proof Caching](../ProofCaching) -- [Proof Tree: linearized mode](../ProofTreeLinearMode) \ No newline at end of file +- [Proof Tree: linearized mode](../ProofTreeLinearMode) +- [Isabelle Translation](../IsabelleTranslation) \ No newline at end of file