Diffusion Isabelle 5930c89d3bf2

merged
5930c89d3bf2
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rISABELLE0d2ea608d223: Added tag Isabelle2023 for changeset b5f3d1051b13
rISABELLE4da1e18a9633: Loads of new material related to porting the Euler Polyhedron Formula from HOL…

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE5930c89d3bf2: merged.Mon, Sep 11, 10:59 PM

Merged Changes

0d2ea608d223 Added tag Isabelle2023 for changeset b5f3d1051b13
Author
makarius
Browse Repository
No Builds
No Audits
b5f3d1051b13 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
71536ae52b16 misc tuning;
Author
makarius
Browse Repository
No Builds
No Audits
0aa741c67086 documentation for the "Document" panel in Isabelle/jEdit;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (129)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

components.sha1

etc/

lib/

Tools/

src/

HOL/

Algebra/

Analysis/

Abstract_Topological_Spaces.thy

Borel_Space.thy

Complex_Analysis_Basics.thy

Convex_Euclidean_Space.thy

Elementary_Topology.thy

Equivalence_Lebesgue_Henstock_Integration.thy

Finite_Product_Measure.thy

Further_Topology.thy

Lebesgue_Measure.thy

Linear_Algebra.thy

Path_Connected.thy

Complex_Analysis/

Cauchy_Integral_Formula.thy

Cauchy_Integral_Theorem.thy

Complex_Singularities.thy

Conformal_Mappings.thy

Contour_Integration.thy

Laurent_Convergence.thy

Residue_Theorem.thy

Riemann_Mapping.thy

Data_Structures/

Array_Braun.thy

Brother12_Set.thy

Tries_Binary.thy

Number_Theory/

Eratosthenes.thy

Probability/

Infinite_Product_Measure.thy

Information.thy

Real_Vector_Spaces.thy

Tools/

ATP/

system_on_tptp.scala

Sledgehammer/

async_manager_legacy.ML

sledgehammer.ML

sledgehammer_prover_atp.ML

Topological_Spaces.thy

Pure/

Admin/

build_history.scala

build_log.scala

build_release.scala

build_status.scala

isabelle_cronjob.scala

Concurrent/

consumer_thread.scala

isabelle_thread.ML

multithreading.ML

single_assignment.ML

synchronized.ML

General/

mercurial.scala

ML/

PIDE/

document_status.scala

query_operation.scala

rendering.scala

System/

components.scala

executable.scala

isabelle_system.scala

message_channel.ML

other_isabelle.scala

Thy/

export_theory.scala

Tools/

build_cluster.scala

check_keywords.scala

dotnet_setup.scala

phabricator.scala

profiling_report.scala

simplifier_trace.scala

spell_checker.scala

task_statistics.scala

Tools/

Code/

Graphview/

mutator_dialog.scala

mutator_event.scala

Metis/

PortableIsabelle.sml

VSCode/

src/

component_vscodium.scala

jEdit/

jedit_base/

jedit_main/

src/

document_dockable.scala

document_model.scala

jedit_sessions.scala

query_dockable.scala

sledgehammer_dockable.scala

symbols_dockable.scala

theories_status.scala

rISABELLE5930c89d3bf2

Admin/components/components.sha1

Admin/components/go

CONTRIBUTORS

NEWS

etc/settings

lib/Tools/scala_build

src/HOL/Algebra/Ring.thy

src/HOL/Analysis/Abstract_Topological_Spaces.thy

src/HOL/Analysis/Affine.thy

src/HOL/Analysis/Borel_Space.thy

src/HOL/Analysis/Complex_Analysis_Basics.thy

src/HOL/Analysis/Convex.thy

src/HOL/Analysis/Convex_Euclidean_Space.thy

src/HOL/Analysis/Elementary_Topology.thy

src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

src/HOL/Analysis/Finite_Product_Measure.thy

src/HOL/Analysis/Further_Topology.thy

src/HOL/Analysis/Homotopy.thy

src/HOL/Analysis/Lebesgue_Measure.thy

src/HOL/Analysis/Linear_Algebra.thy

src/HOL/Analysis/Path_Connected.thy

src/HOL/Analysis/Polytope.thy

src/HOL/Analysis/Starlike.thy

src/HOL/Binomial.thy

src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy

src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy

src/HOL/Complex_Analysis/Complex_Singularities.thy

src/HOL/Complex_Analysis/Conformal_Mappings.thy

src/HOL/Complex_Analysis/Contour_Integration.thy

src/HOL/Complex_Analysis/Laurent_Convergence.thy

src/HOL/Complex_Analysis/Residue_Theorem.thy

src/HOL/Complex_Analysis/Riemann_Mapping.thy

src/HOL/Data_Structures/Array_Braun.thy

src/HOL/Data_Structures/Brother12_Set.thy

src/HOL/Data_Structures/Sorting.thy

src/HOL/Data_Structures/Tries_Binary.thy

src/HOL/Number_Theory/Eratosthenes.thy

src/HOL/Number_Theory/Residues.thy

src/HOL/Probability/Giry_Monad.thy

src/HOL/Probability/Infinite_Product_Measure.thy

src/HOL/Probability/Information.thy

src/HOL/Probability/Levy.thy

src/HOL/Probability/SPMF.thy

src/HOL/Real_Vector_Spaces.thy

src/HOL/Tools/ATP/system_on_tptp.scala

src/HOL/Tools/Sledgehammer/async_manager_legacy.ML

src/HOL/Tools/Sledgehammer/sledgehammer.ML

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

src/HOL/Topological_Spaces.thy

src/Pure/Admin/afp.scala

src/Pure/Admin/build_history.scala

src/Pure/Admin/build_log.scala

src/Pure/Admin/build_release.scala

src/Pure/Admin/build_status.scala

src/Pure/Admin/isabelle_cronjob.scala

src/Pure/Concurrent/consumer_thread.scala

src/Pure/Concurrent/event_timer.ML

src/Pure/Concurrent/future.ML

src/Pure/Concurrent/future.scala

src/Pure/Concurrent/isabelle_thread.ML

src/Pure/Concurrent/multithreading.ML

src/Pure/Concurrent/single_assignment.ML

src/Pure/Concurrent/synchronized.ML

src/Pure/Concurrent/task_queue.ML

src/Pure/Concurrent/timeout.ML

src/Pure/General/json.scala

src/Pure/General/json_api.scala

src/Pure/General/mercurial.scala

src/Pure/General/sql.scala

src/Pure/General/ssh.scala

src/Pure/General/symbol.scala

src/Pure/General/toml.scala

src/Pure/General/word.scala

src/Pure/ML/ml_init.ML

src/Pure/ML/ml_pp.ML

src/Pure/PIDE/command.scala

src/Pure/PIDE/document.scala

src/Pure/PIDE/document_status.scala

src/Pure/PIDE/query_operation.scala

src/Pure/PIDE/rendering.scala

src/Pure/ROOT.ML

src/Pure/ROOT.scala

src/Pure/System/components.scala

src/Pure/System/executable.scala

src/Pure/System/isabelle_system.scala

src/Pure/System/message_channel.ML

src/Pure/System/options.scala

src/Pure/System/other_isabelle.scala

src/Pure/System/platform.scala

src/Pure/System/progress.scala

src/Pure/System/scala.scala

src/Pure/Thy/bibtex.scala

src/Pure/Thy/export.scala

src/Pure/Thy/export_theory.scala

src/Pure/Thy/html.scala

src/Pure/Thy/latex.scala

src/Pure/Tools/build.scala

src/Pure/Tools/build_cluster.scala

src/Pure/Tools/check_keywords.scala

src/Pure/Tools/debugger.ML

src/Pure/Tools/dotnet_setup.scala

src/Pure/Tools/dump.scala

src/Pure/Tools/phabricator.scala

src/Pure/Tools/prismjs.scala

src/Pure/Tools/profiling_report.scala

src/Pure/Tools/server.scala

src/Pure/Tools/simplifier_trace.scala

src/Pure/Tools/spell_checker.scala

src/Pure/Tools/task_statistics.scala

src/Pure/unify.ML

src/Tools/Code/code_scala.ML

src/Tools/Graphview/layout.scala

src/Tools/Graphview/model.scala

src/Tools/Graphview/mutator_dialog.scala

src/Tools/Graphview/mutator_event.scala

src/Tools/Metis/PortableIsabelle.sml

src/Tools/Metis/metis.ML

src/Tools/VSCode/src/component_vscodium.scala

src/Tools/jEdit/jedit_base/plugin.props

src/Tools/jEdit/jedit_main/plugin.props

src/Tools/jEdit/src/document_dockable.scala

src/Tools/jEdit/src/document_model.scala

src/Tools/jEdit/src/jedit_sessions.scala

src/Tools/jEdit/src/query_dockable.scala

src/Tools/jEdit/src/sledgehammer_dockable.scala

src/Tools/jEdit/src/symbols_dockable.scala

src/Tools/jEdit/src/theories_status.scala