# HG changeset patch
# User haftmann
# Date 1278945500 -7200
# Node ID 7371534297a9c554e57424031888288c45234069
# Parent  346caefc9f575056b4c8b9e82efac3d831a2942c
moved auxiliary lemma

diff -r 346caefc9f57 -r 7371534297a9 src/HOL/Imperative_HOL/Relational.thy
--- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:26:48 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:38:20 2010 +0200
@@ -2,10 +2,4 @@
 imports Array Ref
 begin
 
-lemma crel_option_case:
-  assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
-  obtains "x = None" "crel n h h' r"
-        | y where "x = Some y" "crel (s y) h h' r" 
-  using assms unfolding crel_def by (auto split: option.splits)
-
 end
diff -r 346caefc9f57 -r 7371534297a9 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 12 16:26:48 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 12 16:38:20 2010 +0200
@@ -459,6 +459,12 @@
                 else raise(''No empty clause''))
    done)"
 
+lemma crel_option_case:
+  assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
+  obtains "x = None" "crel n h h' r"
+         | y where "x = Some y" "crel (s y) h h' r" 
+  using assms unfolding crel_def by (auto split: option.splits)
+
 lemma res_thm2_Inv:
   assumes res_thm: "crel (res_thm2 a (l, j) cli) h h' rs"
   assumes correct_a: "correctArray r a h"