diff -r ba465fcd0267 -r 8c6226d88ced src/HOL/HOLCF/IOA/ex/TrivEx.thy --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 22:05:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 22:09:44 2015 +0100 @@ -45,7 +45,7 @@ "h_abs n = (n~=0)" axiomatization where - MC_result: "validIOA A_ioa (\\<%(b,a,c). b>)" + MC_result: "validIOA A_ioa (\\\%(b,a,c). b\)" lemma h_abs_is_abstraction: "is_abstraction h_abs C_ioa A_ioa" @@ -61,7 +61,7 @@ apply (simp add: h_abs_def) done -lemma TrivEx_abstraction: "validIOA C_ioa (\\<%(n,a,m). n~=0>)" +lemma TrivEx_abstraction: "validIOA C_ioa (\\\%(n,a,m). n~=0\)" apply (rule AbsRuleT1) apply (rule h_abs_is_abstraction) apply (rule MC_result)