--- a/src/HOLCF/FOCUS/FOCUS.thy Thu Jun 01 23:09:34 2006 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.thy Thu Jun 01 23:53:29 2006 +0200
@@ -9,4 +9,22 @@
imports Fstream
begin
+lemma ex_eqI [intro!]: "? xx. x = xx"
+by auto
+
+lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy"
+by auto
+
+lemma eq_UU_symf: "(UU = f x) = (f x = UU)"
+by auto
+
+lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)"
+by (simp add: slen_empty_eq fstream_exhaust_eq)
+
+lemmas [simp] =
+ slen_less_1_eq fstream_exhaust_slen_eq
+ slen_fscons_eq slen_fscons_less_eq Suc_ile_eq
+
+declare strictI [elim]
+
end