--- a/src/HOL/Boogie/Boogie.thy Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/Boogie/Boogie.thy Fri Nov 06 09:27:20 2009 +0100
@@ -193,8 +193,8 @@
structure Boogie_Axioms = Named_Thms
(
val name = "boogie"
- val description = ("Boogie background axioms" ^
- " loaded along with Boogie verification conditions")
+ val description =
+ "Boogie background axioms loaded along with Boogie verification conditions"
)
*}
setup Boogie_Axioms.setup
@@ -207,8 +207,8 @@
structure Split_VC_SMT_Rules = Named_Thms
(
val name = "split_vc_smt"
- val description = ("Theorems given to the SMT sub-tactic" ^
- " of the split_vc method")
+ val description =
+ "theorems given to the SMT sub-tactic of the split_vc method"
)
*}
setup Split_VC_SMT_Rules.setup
--- a/src/HOL/Boogie/Examples/ROOT.ML Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/Boogie/Examples/ROOT.ML Fri Nov 06 09:27:20 2009 +0100
@@ -1,3 +1,1 @@
-use_thy "Boogie_Max";
-use_thy "Boogie_Dijkstra";
-use_thy "VCC_Max";
+use_thys ["Boogie_Max", "Boogie_Dijkstra", "VCC_Max"];
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Nov 06 09:27:20 2009 +0100
@@ -136,13 +136,11 @@
in get_first is_builtin end
fun lookup_const thy name T =
- let
- val intern = Sign.intern_const thy name
- val is_type_instance = Type.typ_instance o Sign.tsig_of
+ let val intern = Sign.intern_const thy name
in
if Sign.declared_const thy intern
then
- if is_type_instance thy (T, Sign.the_const_type thy intern)
+ if Sign.typ_instance thy (T, Sign.the_const_type thy intern)
then SOME (Const (intern, T))
else error ("Boogie: function already declared with different type: " ^
quote name)
--- a/src/HOL/SMT/Examples/SMT_Examples.thy Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Fri Nov 06 09:27:20 2009 +0100
@@ -5,7 +5,7 @@
header {* Examples for the 'smt' tactic. *}
theory SMT_Examples
-imports "../SMT"
+imports SMT
begin
declare [[smt_solver=z3, z3_proofs=true]]