# HG changeset patch
# User wenzelm
# Date 1606474223 -3600
# Node ID b808eddc83cf2f9c2782bb6595fedd936a5ae78e
# Parent  082200ee003d60a3e6028600d6c0fac0777b8682
clarified file names;

diff -r 082200ee003d -r b808eddc83cf src/HOL/SMT_Examples/Boogie.thy
--- a/src/HOL/SMT_Examples/Boogie.thy	Fri Nov 27 11:41:43 2020 +0100
+++ b/src/HOL/SMT_Examples/Boogie.thy	Fri Nov 27 11:50:23 2020 +0100
@@ -6,7 +6,7 @@
 
 theory Boogie
 imports Main
-keywords "boogie_file" :: thy_load ("b2i")
+keywords "boogie_file" :: thy_load
 begin
 
 text \<open>
@@ -58,19 +58,19 @@
 external_file \<open>Boogie_Max.certs\<close>
 declare [[smt_certificates = "Boogie_Max.certs"]]
 
-boogie_file \<open>Boogie_Max\<close>
+boogie_file \<open>Boogie_Max.b2i\<close>
 
 
 external_file \<open>Boogie_Dijkstra.certs\<close>
 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
 
-boogie_file \<open>Boogie_Dijkstra\<close>
+boogie_file \<open>Boogie_Dijkstra.b2i\<close>
 
 
 declare [[z3_extensions = true]]
 external_file \<open>VCC_Max.certs\<close>
 declare [[smt_certificates = "VCC_Max.certs"]]
 
-boogie_file \<open>VCC_Max\<close>
+boogie_file \<open>VCC_Max.b2i\<close>
 
 end