# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308881898 -32400
# Node ID a95a497e1f4f99ec65efd9a8f6bf142a8c3ff129
# Parent  fd4fa6df22d114dcef548e85982e8833ac461264
Make examples work with non-precompiled image

diff -r fd4fa6df22d1 -r a95a497e1f4f Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Fri Jun 24 11:15:22 2011 +0900
+++ b/Nominal/Ex/CPS/Lt.thy	Fri Jun 24 11:18:18 2011 +0900
@@ -1,6 +1,6 @@
 header {* The Call-by-Value Lambda Calculus *}
 theory Lt
-imports Nominal2
+imports "../../Nominal2"
 begin
 
 atom_decl name
diff -r fd4fa6df22d1 -r a95a497e1f4f Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Fri Jun 24 11:15:22 2011 +0900
+++ b/Nominal/Ex/SFT/Consts.thy	Fri Jun 24 11:18:18 2011 +0900
@@ -1,5 +1,6 @@
 header {* Constant definitions *}
-theory Consts imports Utils Lambda begin
+
+theory Consts imports Utils begin
 
 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"
 where
diff -r fd4fa6df22d1 -r a95a497e1f4f Nominal/Ex/SFT/Lambda.thy
--- a/Nominal/Ex/SFT/Lambda.thy	Fri Jun 24 11:15:22 2011 +0900
+++ b/Nominal/Ex/SFT/Lambda.thy	Fri Jun 24 11:18:18 2011 +0900
@@ -1,6 +1,6 @@
 header {* Definition of Lambda terms and convertibility *}
 
-theory Lambda imports Nominal2 begin
+theory Lambda imports "../../Nominal2" begin
 
 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"
   unfolding fresh_def by blast
diff -r fd4fa6df22d1 -r a95a497e1f4f Nominal/Ex/SFT/Theorem.thy
--- a/Nominal/Ex/SFT/Theorem.thy	Fri Jun 24 11:15:22 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy	Fri Jun 24 11:18:18 2011 +0900
@@ -1,4 +1,5 @@
 header {* The main lemma about Num and the Second Fixed Point Theorem *}
+
 theory Theorem imports Consts begin
 
 lemmas [simp] = b3[OF bI] b1 b4 b5 supp_Num[unfolded Num_def supp_ltgt] Num_def lam.fresh[unfolded fresh_def] fresh_def b6
diff -r fd4fa6df22d1 -r a95a497e1f4f Nominal/Ex/SFT/Utils.thy
--- a/Nominal/Ex/SFT/Utils.thy	Fri Jun 24 11:15:22 2011 +0900
+++ b/Nominal/Ex/SFT/Utils.thy	Fri Jun 24 11:18:18 2011 +0900
@@ -1,4 +1,5 @@
 header {* Utilities for defining constants and functions *}
+
 theory Utils imports Lambda begin
 
 lemma beta_app: