From 140ae6d623c76b0d1c9e9af17da4d570b52606b2 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 25 Feb 2021 08:48:04 +0000 Subject: [PATCH] Import of AFP for Isabelle 2021. --- .../Stateful_Protocol_Model.thy | 2 +- Automated_Stateful_Protocol_Verification/document/root.tex | 6 ++---- Automated_Stateful_Protocol_Verification/trac/trac.thy | 2 +- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy b/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy index 239adef..7810497 100644 --- a/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy +++ b/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy @@ -3289,7 +3289,7 @@ proof - thus ?thesis by simp qed (use 2(3) in simp) moreover have "\u u'. T = [u,u']" - using 2(2) by (metis (no_types) length_0_conv length_Suc_conv) + using 2(2) by (metis (no_types, lifting) Suc_length_conv length_0_conv) ultimately show ?thesis using Fun 2(1,2) by force qed qed diff --git a/Automated_Stateful_Protocol_Verification/document/root.tex b/Automated_Stateful_Protocol_Verification/document/root.tex index 2a851b7..b1834c4 100644 --- a/Automated_Stateful_Protocol_Verification/document/root.tex +++ b/Automated_Stateful_Protocol_Verification/document/root.tex @@ -1,6 +1,6 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright] {scrreprt} -\usepackage[USenglish]{babel} +\usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym} \usepackage{booktabs} @@ -22,8 +22,6 @@ \begingroup% \def\isacharunderscore{\textunderscore}% \section{#1 (\thy)}% - \def\isacharunderscore{-}% - \expandafter\label{sec:\isabellecontext}% \endgroup% } @@ -119,7 +117,7 @@ present examples (\autoref{cha:examples}). \paragraph{Acknowledgments} -This work was supported by the Sapere-Aude project ``Composec: Secure Composition of Distributed Systems'', grant 4184-00334B of the Danish Council for Independent Research. +This work was supported by the Sapere-Aude project ``Composec: Secure Composition of Distributed Systems'', grant 4184-00334B of the Danish Council for Independent Research, by the EU H2020 project no. 700321 ``LIGHTest: Lightweight Infrastructure for Global Heterogeneous Trust management in support of an open Ecosystem of Trust schemes'' (lightest.eu) and by the ``CyberSec4Europe'' European Union's Horizon 2020 research and innovation programme under grant agreement No 830929. \clearpage diff --git a/Automated_Stateful_Protocol_Verification/trac/trac.thy b/Automated_Stateful_Protocol_Verification/trac/trac.thy index 27958b1..191c613 100644 --- a/Automated_Stateful_Protocol_Verification/trac/trac.thy +++ b/Automated_Stateful_Protocol_Verification/trac/trac.thy @@ -1661,7 +1661,7 @@ structure trac = struct in Path.implode (if (Path.is_absolute filename) then filename - else Path.append master_dir filename) + else master_dir + filename) end (* fun exec {trac_path, error_detail} filename = let