Skip to content

Fixing some broken links and adding menu entry for IsabelleTranslation #46

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

Fixing some broken links and adding menu entry for IsabelleTranslation #46

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
172be49
fix broken links and add IsabelleTranslation menu entry
BookWood7th May 26, 2025
7f0c186
Merge branch 'KeYProject:master' into master
BookWood7th May 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions docs/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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/)
Expand Down
8 changes: 4 additions & 4 deletions docs/user/IsabelleTranslation/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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.
Expand All @@ -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
Expand Down
3 changes: 2 additions & 1 deletion docs/user/UiFeatures/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,5 @@
- [Node Differences](../NodeDiff)
- [Proof Slicing](../ProofSlicing)
- [Proof Caching](../ProofCaching)
- [Proof Tree: linearized mode](../ProofTreeLinearMode)
- [Proof Tree: linearized mode](../ProofTreeLinearMode)
- [Isabelle Translation](../IsabelleTranslation)