--- a/thys/UF.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/UF.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -14,10 +14,6 @@
 subsection {* The construction of component functions *}
 
 text {*
-  This section constructs a set of component functions used to construct @{text "rec_F"}.
-  *}
-
-text {*
   The recursive function used to do arithmatic addition.
 *}
 definition rec_add :: "recf"
@@ -2428,7 +2424,6 @@
      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]],
      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],
      Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"
-  thm embranch_lemma
   have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
                          = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
     apply(rule_tac embranch_lemma )
@@ -2644,8 +2639,6 @@
   where
   "rght c = lo c (Pi 2)"
 
-thm Prime.simps
-
 fun inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "inpt m xs = trpl 0 1 (strt xs)"
@@ -3103,7 +3096,6 @@
         apply(rule_tac calc_pr_zero, simp)
         using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"]
         apply(simp add: rec_exec.simps, simp, simp, simp)
-        thm calc_pr_ind
         apply(rule_tac rk = "rec_exec (Pr n f g)
                (butlast xs@[last xs - Suc 0])" in calc_pr_ind)
         using ind2[of "rec_exec (Pr n f g)
@@ -3540,7 +3532,6 @@
 subsection {* Relating interperter functions to the execution of TMs *}
 
 lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
-term trpl
 
 lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
 apply(simp add: fetch.simps)
@@ -3586,7 +3577,6 @@
 apply(simp)
 done
 
-term set_of
 lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
 proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
       rule_tac classical, simp)