--- a/Unused.thy	Wed Oct 28 16:48:57 2009 +0100
+++ b/Unused.thy	Wed Oct 28 17:17:21 2009 +0100
@@ -1,3 +1,5 @@
+(*notation ( output) "prop" ("#_" [1000] 1000) *)
+notation ( output) "Trueprop" ("#_" [1000] 1000)
 
 ML {*
   fun dest_cbinop t =
@@ -72,3 +74,15 @@
 lemma trueprop_cong:
   shows "(a ≡ b) ⟹ (Trueprop a ≡ 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)"
+  using a
+  apply (rule_tac allI)
+  apply (induct_tac "l")
+  apply (simp)
+  apply (metis)
+  done
+