ProtocolSecurity
/
isabelle-ofmc
Archived
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Generated thy files for Isabelle 2015.

This commit is contained in:
Achim D. Brucker 2016-08-02 12:49:06 +01:00
parent 9ef8e90bd7
commit bb1c93b00e
1 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/encoder/ofmc_thygen.sml
View File

@ -71,7 +71,7 @@ fun gen_header ofmcfp =
else filename
end
in
"header {* Analysing "^(protocol)^" *}\n"
"chapter {* Analysing "^(protocol)^" *}\n"
^"(* *********************************** \n"
^" This file is automatically generated from the AnB file \""
^(source_of ofmcfp)^"\".\n"
@ -331,16 +331,14 @@ fun gen_fp ofmcfp =
in
if inner_quantification
then
( "constdefs"
^" "^protocolFp^"::\"Fact set\""
^"\""^protocolFp^" == {m. (\n"
( "definition\n"
^"\""^protocolFp^" = {m. (\n"
^" ("^(string_of_fp_fact ofmcfp (hd facts)^")\n")
^(String.concat (map (fn f => " | ("^(string_of_fp_fact ofmcfp f)^")\n") (tl facts) ))
^")}\"\n")
else
( "constdefs"
^" "^protocolFp^"::\"Fact set\""
^"\""^protocolFp^" == {m. ( ? "^(String.concat (map (fn f => string_of_cmsg f^" ") (#1 outer_ex )))^".\n"
( "definition\n"
^"\""^protocolFp^" = {m. ( ? "^(String.concat (map (fn f => string_of_cmsg f^" ") (#1 outer_ex )))^".\n"
^" ("^(string_of_fp_fact' ofmcfp (hd (#2 outer_ex ))^")\n")
^(String.concat (map (fn f => " | ("^(string_of_fp_fact' ofmcfp f)^")\n") (tl (#2 outer_ex )) ))
^")}\"\n")