summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/BoogieDriver/BoogieDriver.sscproj4
-rw-r--r--Source/Provers/Isabelle/AssemblyInfo.ssc6
-rw-r--r--Source/Provers/Isabelle/Isabelle.sscproj4
-rw-r--r--Source/Provers/Isabelle/Prover.ssc24
4 files changed, 21 insertions, 17 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.sscproj b/Source/BoogieDriver/BoogieDriver.sscproj
index 6be752c9..d2818f25 100644
--- a/Source/BoogieDriver/BoogieDriver.sscproj
+++ b/Source/BoogieDriver/BoogieDriver.sscproj
@@ -122,6 +122,10 @@
Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
Private="true"
/>
+ <Reference Name="Isabelle"
+ Project="{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}"
+ Private="true"
+ />
</References>
</Build>
<Files>
diff --git a/Source/Provers/Isabelle/AssemblyInfo.ssc b/Source/Provers/Isabelle/AssemblyInfo.ssc
index df4952da..ba2375e7 100644
--- a/Source/Provers/Isabelle/AssemblyInfo.ssc
+++ b/Source/Provers/Isabelle/AssemblyInfo.ssc
@@ -3,15 +3,11 @@
using System.Reflection;
using System.Runtime.CompilerServices;
-[assembly: AssemblyVersion("4.0.0.0")]
-[assembly: AssemblyFileVersion("4.0.0.0")]
+[assembly: AssemblyKeyFile("..\\..\\InterimKey.snk")]
[assembly: AssemblyTitle("Boogie back-end for Isabelle")]
[assembly: AssemblyDescription("Boogie back-end for the interactive"
+ " theorem prover Isabelle")]
-[assembly: AssemblyConfiguration("Release")]
[assembly: AssemblyCompany("TU München")]
[assembly: AssemblyProduct("HOL-Boogie")]
[assembly: AssemblyCopyright("Copyright © TU München 2009")]
-[assembly: AssemblyTrademark("")]
-[assembly: AssemblyCulture("")]
diff --git a/Source/Provers/Isabelle/Isabelle.sscproj b/Source/Provers/Isabelle/Isabelle.sscproj
index 0e4a5c58..8f694208 100644
--- a/Source/Provers/Isabelle/Isabelle.sscproj
+++ b/Source/Provers/Isabelle/Isabelle.sscproj
@@ -93,6 +93,10 @@
SubType="Code"
RelPath="Prover.ssc"
/>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="..\..\version.ssc"
+ />
</Include>
</Files>
</XEN>
diff --git a/Source/Provers/Isabelle/Prover.ssc b/Source/Provers/Isabelle/Prover.ssc
index 02bd2d36..9b91cd63 100644
--- a/Source/Provers/Isabelle/Prover.ssc
+++ b/Source/Provers/Isabelle/Prover.ssc
@@ -12,18 +12,18 @@ modification, are permitted provided that the following conditions are met:
* Neither the name of the Technische Universitaet Muenchen nor the names of
its contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
-AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
-ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
-LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
-CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
-SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
-INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
-CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
-ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
-POSSIBILITY OF SUCH DAMAGE.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
*/
using System;