src/HOL/Main.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 61955 e96292f32c3c child 62921 499a63c30d55 permissions -rw-r--r--
generalize more theorems to support enat and ennreal
 wenzelm@60758 1 section \Main HOL\ wenzelm@12024 2 nipkow@15131 3 theory Main hoelzl@60036 4 imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter nipkow@15131 5 begin wenzelm@9650 6 wenzelm@60758 7 text \ wenzelm@29304 8 Classical Higher-order Logic -- only ``Main'', excluding real and wenzelm@29304 9 complex numbers etc. wenzelm@60758 10 \ wenzelm@29304 11 wenzelm@60758 12 text \See further @{cite "Nipkow-et-al:2002:tutorial"}\ haftmann@25964 13 haftmann@51112 14 no_notation haftmann@51112 15 bot ("\") and haftmann@51112 16 top ("\") and haftmann@51112 17 inf (infixl "\" 70) and haftmann@51112 18 sup (infixl "\" 65) and haftmann@51112 19 Inf ("\_" [900] 900) and blanchet@55057 20 Sup ("\_" [900] 900) and blanchet@55065 21 ordLeq2 (infix "<=o" 50) and blanchet@55065 22 ordLeq3 (infix "\o" 50) and blanchet@55065 23 ordLess2 (infix "(_,/ _)\") haftmann@51112 30 blanchet@55087 31 hide_const (open) blanchet@58152 32 czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect blanchet@58152 33 fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift blanchet@58353 34 shift proj id_bnf blanchet@58353 35 blanchet@58353 36 hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV blanchet@55087 37 wenzelm@61955 38 no_syntax haftmann@51112 39 "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) haftmann@51112 40 "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) haftmann@51112 41 "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) haftmann@51112 42 "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) haftmann@51112 43 wenzelm@9650 44 end