HomeIsabelle/Phabricator
Diffusion afp-devel 28ce3268cde2

CTR and ETTS: integration with fd5f62176987
28ce3268cde2
Actions

Description

CTR and ETTS: integration with fd5f62176987

Details

Provenance
user9716869 <user9716869@gmail.com>Authored on
Parents
rAFPf8ba1eaa5cec: adapted QHLProver to isabelle-dev/409ca22dee4c
Branches
Unknown
Tags
Unknown

Changes (8)

PathSize
thys/
Conditional_Transfer_Rule/
UD/
Types_To_Sets_Extension/
ETTS/
Tests/
Examples/
SML_Relativization/
Lattices/
Simple_Orders/

rAFP28ce3268cde2

View Options

thys/Conditional_Transfer_Rule/UD/UD.ML

Loading...
View Options

thys/Types_To_Sets_Extension/ETTS/ETTS_Algorithm.ML

Loading...
View Options

thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML

Loading...
View Options

thys/Types_To_Sets_Extension/Examples/Introduction.thy

Loading...
View Options

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy

Loading...
View Options

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Semilattices.thy

Loading...
View Options

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy

Loading...
View Options

thys/Types_To_Sets_Extension/ROOT

Loading...