isabelle: src/HOL/Library/Cardinal_Notations.thy@637aa8e93cd7 (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
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	8	section \<open>Cardinal Notations\<close>
55070 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	wenzelm
	Fri, 28 Apr 2017 13:21:03 +0200
changeset 65604	637aa8e93cd7
parent 60500	903bb1495239
permissions	-rw-r--r--