wneuper/isa: doc-src/Intro/arith.thy@20e3616b2d9c

doc-src/Intro/arith.thy

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 105	216d6ed87399
permissions	-rw-r--r--

prepare reactivation of isac-update-Isa09-2

     1 Arith = FOL +

     2 classes arith < term

     3 consts  "0"     :: "'a::arith"                  ("0")

     4         "1"     :: "'a::arith"                  ("1")

     5         "+"     :: "['a::arith,'a] => 'a"       (infixl 60)

     6 end

wneuper/isa