--- a/thys/uncomputable.thy	Sun Jan 27 17:15:38 2013 +0000
+++ b/thys/uncomputable.thy	Sun Jan 27 20:01:13 2013 +0000
@@ -49,7 +49,7 @@
                 (R, 2), (R, 2), (L, 5), (W0, 4),
                 (R, 0), (L, 5)]"
 
-idefinition 
+definition 
   tcopy :: "instr list"
 where
   "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
@@ -137,7 +137,7 @@
 
 lemma init_halt: 
   "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
-proof(rule_tac LE = init_LE in halt_lemma)
+proof(rule_tac LE = init_LE in halt_lemma) 
   show "wf init_LE" by(simp add: wf_begin_le)
 next
   assume h: "0 < x"