isabelle: src/HOL/Numeral.thy@f8353c722d4e (annotated)

6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	1	(* Title: HOL/Numeral.thy
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	2	ID: $Id$
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	3	Author: Larry Paulson and Markus Wenzel
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	4
9410 612ee826a409 removed selector syntax -- improper tuples are broken beyond repair :-( wenzelm parents: 9358 diff changeset	5	Generic numerals represented as twos-complement bit strings.
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	6	*)
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	7
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	8	theory Numeral = Datatype
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	9	files "Tools/numeral_syntax.ML":
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	10
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	11	datatype
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	12	bin = Pls
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	13	\| Min
9358 973672495414 added syntax for proper / improper selector functions; wenzelm parents: 9035 diff changeset	14	\| Bit bin bool (infixl "BIT" 90)
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	15
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	16	axclass
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	17	number < "term" (for numeric types: nat, int, real, ...)
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	18
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	19	consts
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	20	number_of :: "bin => 'a::number"
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	21
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	22	syntax
9358 973672495414 added syntax for proper / improper selector functions; wenzelm parents: 9035 diff changeset	23	"_Numeral" :: "xnum => 'a" ("_")
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	24
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	25	setup NumeralSyntax.setup
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	26
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	27	end

author	paulson
	Tue, 01 May 2001 17:16:32 +0200
changeset 11276	f8353c722d4e
parent 9410	612ee826a409
child 11488	4ff900551340
permissions	-rw-r--r--