isabelle: src/HOL/Library/Cardinal_Notations.thy@5d147e1e18d1 (annotated)

55075 b3d0a02a756d dissolved BNF session blanchet parents: 55070 diff changeset	1	(* Title: HOL/Library/Cardinal_Notations.thy
55070 235c7661a96b rationalized dependencies blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
235c7661a96b rationalized dependencies blanchet parents: diff changeset	3	Copyright 2013
235c7661a96b rationalized dependencies blanchet parents: diff changeset	4
235c7661a96b rationalized dependencies blanchet parents: diff changeset	5	Cardinal notations.
235c7661a96b rationalized dependencies blanchet parents: diff changeset	6	*)
235c7661a96b rationalized dependencies blanchet parents: diff changeset	7
235c7661a96b rationalized dependencies blanchet parents: diff changeset	8	header {* Cardinal Notations *}
235c7661a96b rationalized dependencies blanchet parents: diff changeset	9
235c7661a96b rationalized dependencies blanchet parents: diff changeset	10	theory Cardinal_Notations
235c7661a96b rationalized dependencies blanchet parents: diff changeset	11	imports Main
235c7661a96b rationalized dependencies blanchet parents: diff changeset	12	begin
235c7661a96b rationalized dependencies blanchet parents: diff changeset	13
235c7661a96b rationalized dependencies blanchet parents: diff changeset	14	notation
235c7661a96b rationalized dependencies blanchet parents: diff changeset	15	ordLeq2 (infix "<=o" 50) and
235c7661a96b rationalized dependencies blanchet parents: diff changeset	16	ordLeq3 (infix "\<le>o" 50) and
235c7661a96b rationalized dependencies blanchet parents: diff changeset	17	ordLess2 (infix "<o" 50) and
235c7661a96b rationalized dependencies blanchet parents: diff changeset	18	ordIso2 (infix "=o" 50) and
55087 252c7fec4119 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test) blanchet parents: 55078 diff changeset	19	card_of ("\|_\|") and
55128 6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	20	BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	21	BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	22	BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	23
6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	24	abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	25	abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	26	abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
6e16d2dd4f14 hide 'csum' etc. blanchet parents: 55087 diff changeset	27	abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
55070 235c7661a96b rationalized dependencies blanchet parents: diff changeset	28
235c7661a96b rationalized dependencies blanchet parents: diff changeset	29	end

author	paulson <lp15@cam.ac.uk>
	Fri, 21 Mar 2014 15:36:00 +0000
changeset 56238	5d147e1e18d1
parent 55128	6e16d2dd4f14
child 58881	b9556a055632
permissions	-rw-r--r--