HomeIsabelle/Phabricator
Diffusion afp-devel e1c3276c598b

New entry: Dedekind_Real
e1c3276c598b
Actions

Description

New entry: Dedekind_Real

Details

Provenance
nipkowAuthored on
Parents
rAFPc296f652adc9: New entry Ackermann_not_PR, from distribution
Branches
Unknown
Tags
Unknown

Changes (34)

PathSize
metadata/

rAFPe1c3276c598b

View Options

metadata/metadata

Loading...
View Options

thys/Dedekind_Real/Dedekind_Real.thy

Loading...
View Options

thys/Dedekind_Real/ROOT

Loading...
View Options

thys/Dedekind_Real/document/root.bib

Loading...
View Options

thys/Dedekind_Real/document/root.tex

Loading...
View Options

thys/ROOTS

Loading...
View Options

web/entries/Ackermanns_not_PR.html

Loading...
View Options

web/entries/Cartan_FP.html

Loading...
View Options

web/entries/Dedekind_Real.html

Loading...
View Options

web/entries/Finite_Automata_HF.html

Loading...
View Options

web/entries/FunWithTilings.html

Loading...
View Options

web/entries/Green.html

Loading...
View Options

web/entries/HereditarilyFinite.html

Loading...
View Options

web/entries/Impossible_Geometry.html

Loading...
View Options

web/entries/Incompleteness.html

Loading...
View Options

web/entries/Nash_Williams.html

Loading...
View Options

web/entries/Ordinal_Partitions.html

Loading...
View Options

web/entries/Prime_Number_Theorem.html

Loading...
View Options

web/entries/Quaternions.html

Loading...
View Options

web/entries/Real_Power.html

Loading...
View Options

web/entries/Roth_Arithmetic_Progressions.html

Loading...
View Options

web/entries/Source_Coding_Theorem.html

Loading...
View Options

web/entries/Special_Function_Bounds.html

Loading...
View Options

web/entries/Szemeredi_Regularity.html

Loading...
View Options

web/entries/ZFC_in_HOL.html

Loading...
View Options

web/index.html

Loading...
View Options

web/rss.xml

Loading...
View Options

web/statistics.html

Loading...
View Options

web/topics.html

Loading...