diff -r 5b01f7c233f8 -r a33d3040bf7e thys/ProofAutomation.thy
--- a/thys/ProofAutomation.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-theory ProofAutomation
-imports Main
-begin
-
-lemma "\<forall>x. \<exists>y. x = y"
-by auto
-
-lemma "A \<subseteq> B \<inter> C \<Longrightarrow> A \<subseteq> B \<union> C"
-by auto
-
-lemma "\<lbrakk> \<forall> xs \<in> A. \<exists> ys. xs = ys @ ys; us \<in> A \<rbrakk> \<Longrightarrow> \<exists>n. length us = n+n"
-by fastforce
-
-lemma "\<lbrakk>xs @ ys = ys @ xs; length xs = length ys \<rbrakk> \<Longrightarrow> xs = ys"
-by auto
-
-lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c\<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c"
-by arith
-
-lemma "\<lbrakk> (a::nat) \<le> b; b \<le> c; c \<le> d; d \<le> e \<rbrakk> \<Longrightarrow> a \<le> e"
-by (blast intro: le_trans)
-
-lemma "Suc(Suc(Suc a)) \<le> b \<Longrightarrow> a \<le> b"
-by(blast dest: Suc_leD)
-
-inductive ev :: "nat \<Rightarrow> bool" where
-ev0: "ev 0" |
-evSS: "ev n \<Longrightarrow> ev (n + 2)"
-
-fun even :: "nat \<Rightarrow> bool" where
-"even 0 = True" |
-"even (Suc 0) = False" |
-"even (Suc(Suc n)) = even n"
-
-lemma "ev m \<Longrightarrow> even m"
-