src/HOL/ex/Abstract_NAT.thy
changeset 19363 667b5ea637dd
parent 19087 8d83af663714
child 20485 3078fd2eec7b
     1.1 --- a/src/HOL/ex/Abstract_NAT.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/ex/Abstract_NAT.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -37,8 +37,8 @@
     1.4      Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
     1.5        (succ m, r m n) \<in> REC zero succ e r"
     1.6  
     1.7 -abbreviation (in NAT) (output)
     1.8 -  "Rec = REC zero succ"
     1.9 +abbreviation (in NAT)
    1.10 +  "Rec == REC zero succ"
    1.11  
    1.12  lemma (in NAT) Rec_functional:
    1.13    fixes x :: 'n