--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy Fri Oct 12 15:52:45 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy Fri Oct 12 15:52:55 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"