--- a/Unused.thy	Mon Nov 09 15:40:43 2009 +0100
+++ b/Unused.thy	Tue Nov 10 09:32:16 2009 +0100
@@ -72,13 +72,13 @@
 
 
 lemma trueprop_cong:
-  shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)"
+  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
   by auto
 
 lemma list_induct_hol4:
-  fixes P :: "'a list ⇒ bool"
-  assumes a: "((P []) ∧ (∀t. (P t) ⟶ (∀h. (P (h # t)))))"
-  shows "∀l. (P l)"
+  fixes P :: "'a list \<Rightarrow> bool"
+  assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+  shows "\<forall>l. (P l)"
   using a
   apply (rule_tac allI)
   apply (induct_tac "l")
@@ -93,3 +93,7 @@
     val ((_, [th']), _) = Variable.import true [th] ctxt;
   in th' end);
 *}
+
+(*lemma equality_twice:
+  "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+by auto*)