merged

--- a/src/Doc/ProgProve/Isar.thy	Fri Oct 12 21:39:58 2012 +0200
+++ b/src/Doc/ProgProve/Isar.thy	Fri Oct 12 21:51:25 2012 +0200
@@ -736,8 +736,8 @@
 proposition to be proved in each case is not the whole implication but only
 its conclusion; the premises of the implication are immediately made
 assumptions of that case. That is, if in the above proof we replace
-\isacom{show}~@{text"P(n)"} by
-\mbox{\isacom{show}~@{text"A(n) \<Longrightarrow> P(n)"}}
+\isacom{show}~@{text"\"P(n)\""} by
+\mbox{\isacom{show}~@{text"\"A(n) \<Longrightarrow> P(n)\""}}
 then \isacom{case}~@{text 0} stands for
 \begin{quote}
 \isacom{assume} \ @{text"0: \"A(0)\""}\\

--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy	Fri Oct 12 21:39:58 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy	Fri Oct 12 21:51:25 2012 +0200
@@ -173,8 +173,12 @@
 lemma subtr_StepL:
 assumes r: "root tr1 \<in> ns" and tr12: "Inr tr1 \<in> cont tr2" and s: "subtr ns tr2 tr3"
 shows "subtr ns tr1 tr3"
-apply(rule subtr_trans[OF _ s]) apply(rule Step[of tr2 ns tr1 tr1])
-by (metis assms subtr_rootL_in Refl)+
+apply(rule subtr_trans[OF _ s])
+apply(rule Step[of tr2 ns tr1 tr1])
+apply(rule subtr_rootL_in[OF s])
+apply(rule Refl[OF r])
+apply(rule tr12)
+done
 
 (* alternative definition: *)
 inductive subtr2 where
@@ -220,8 +224,12 @@
 lemma subtr2_StepR:
 assumes r: "root tr3 \<in> ns" and tr23: "Inr tr2 \<in> cont tr3" and s: "subtr2 ns tr1 tr2"
 shows "subtr2 ns tr1 tr3"
-apply(rule subtr2_trans[OF s]) apply(rule Step[of _ _ tr3])
-by (metis assms subtr2_rootR_in Refl)+
+apply(rule subtr2_trans[OF s])
+apply(rule Step[of _ _ tr3])
+apply(rule subtr2_rootR_in[OF s])
+apply(rule tr23)
+apply(rule Refl[OF r])
+done
 
 lemma subtr_subtr2:
 "subtr = subtr2"
@@ -311,7 +319,7 @@
 corollary Itr_subtr_cont:
 "Itr ns tr = {root tr' | tr'. subtr ns tr' tr}"
 unfolding Itr_def apply safe
-  apply (metis (lifting, mono_tags) UnionI inItr_subtr mem_Collect_eq vimageI2)
+  apply (metis (lifting, mono_tags) inItr_subtr)
   by (metis inItr.Base subtr_inItr subtr_rootL_in)
 
 
@@ -512,7 +520,7 @@
 "hsubst \<equiv> unfold hsubst_r hsubst_c"
 
 lemma finite_hsubst_c: "finite (hsubst_c n)"
-unfolding hsubst_c_def by (metis finite_cont)
+unfolding hsubst_c_def by (metis (full_types) finite_cont)
 
 lemma root_hsubst[simp]: "root (hsubst tr) = root tr"
 using unfold(1)[of hsubst_r hsubst_c tr] unfolding hsubst_def hsubst_r_def by simp
@@ -703,7 +711,7 @@
   apply(rule exI[of _ g])
   using f deftr_simps(1) unfolding g_def reg_def apply safe
     apply (metis (lifting) inItr.Base subtr_inItr subtr_rootL_in)
-    by (metis (full_types) inItr_subtr subtr_subtr2)
+    by (metis (full_types) inItr_subtr)
 qed auto
 
 lemma reg_root:
@@ -823,7 +831,7 @@
     show ?thesis apply(rule exI[of _ nl]) using path.Base unfolding nl Nil by simp
   next
     case (Cons n1 nl2)
-    hence p1: "path f nl1" by (metis list.simps nl p_nl path_post)
+    hence p1: "path f nl1" by (metis list.simps(3) nl p_nl path_post)
     show ?thesis
     proof(cases "n \<in> set nl1")
       case False
@@ -1132,7 +1140,7 @@
        \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
 unfolding Fr_def
 using In inFr.Base regular_inFr[OF assms] apply safe
-apply (simp, metis (full_types) UnionI mem_Collect_eq)
+apply (simp, metis (full_types) mem_Collect_eq)
 apply simp
 by (simp, metis (lifting) inFr_Ind_minus insert_Diff)
 

--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy	Fri Oct 12 21:39:58 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy	Fri Oct 12 21:51:25 2012 +0200
@@ -11,15 +11,15 @@
 imports Tree
 begin
 
-
+no_notation plus_class.plus (infixl "+" 65)
+no_notation Sublist.parallel (infixl "\<parallel>" 50)
+    
 consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
 
 axiomatization where
     Nplus_comm: "(a::N) + b = b + (a::N)"
 and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
 
-
-
 section{* Parallel composition *}
 
 fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"