Diffusion Isabelle ab8310c0e6d9

merged
ab8310c0e6d9
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rISABELLE8122e865687e: fixed lemma name
rISABELLE37894dff0111: More material from the HOL Light metric space library

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rISABELLEab8310c0e6d9: merged.Wed, May 17, 9:00 AM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

8122e865687e fixed lemma name
Author
desharna
Browse Repository
No Builds
No Audits
0252d635bfb2 redefined FSet.fmember as an abbreviation based on Set.member
Author
desharna
Browse Repository
No Builds
No Audits
f40bc75b2a3f replaced some lemmas' implicit formulas by explicit ones to avoid silent changes
Author
desharna
Browse Repository
No Builds
No Audits
300537844bb7 merged
Author
makarius
Browse Repository
No Builds
No Audits
35439ca0133c proper setup for rule attribute;
Author
makarius
Browse Repository
No Builds
No Audits
4d9349989d94 more uniform simproc_setup: avoid vacuous abstraction over morphism, which…
Author
makarius
Browse Repository
No Builds
No Audits
2cd7e5518d0d clarified output of embedded values, e.g. for 'print_locale';
Author
makarius
Browse Repository
No Builds
No Audits
2ea20bb1493c tuned: more antiquotations;
Author
makarius
Browse Repository
No Builds
No Audits
838198d17a40 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
bc42c074e58f tuned signature: more position information;
Author
makarius
Browse Repository
No Builds
No Audits
c3efa0b63d2e tuned;
Author
makarius
Browse Repository
No Builds
No Audits
cec875dcc59e Finally, the abstract metric space development
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
070703d83cfe merged
Author
makarius
Browse Repository
No Builds
No Audits
ec1c0daa3fbd misc tuning and clarification;
Author
makarius
Browse Repository
No Builds
No Audits
79ad3181071b tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
52d071212a7a tuned;
Author
makarius
Browse Repository
No Builds
No Audits
3fde7a52c650 tuned --- Token.make_string / Token.assign are value-oriented;
Author
makarius
Browse Repository
No Builds
No Audits
90b64ffc48a3 more documentation;
Author
makarius
Browse Repository
No Builds
No Audits
5edd5b12017d tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
dd7bb7f99ad5 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
f0aca0506531 more robust context: fail immediately via Morphism.the_theory, instead of…
Author
makarius
Browse Repository
No Builds
No Audits
3357bc875b11 prefer static simpset;
Author
makarius
Browse Repository
No Builds
No Audits
a51d2e96203e omit pointless morphism in global theory;
Author
makarius
Browse Repository
No Builds
No Audits
40db83793cea more operations;
Author
makarius
Browse Repository
No Builds
No Audits
b0bcba8afdd8 more careful treatment of context for method source;
Author
makarius
Browse Repository
No Builds
No Audits
270e85124a9a clarified context;
Author
makarius
Browse Repository
No Builds
No Audits
35a86345de48 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
5c3e8e6f430a remove pointless context setup (see also b2e449c155a4);
Author
makarius
Browse Repository
No Builds
No Audits
b2e449c155a4 more careful reset_context for stored entity;
Author
makarius
Browse Repository
No Builds
No Audits
15ab73949713 more careful reset/set_context for stored declarations;
Author
makarius
Browse Repository
No Builds
No Audits
073826f50e14 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
b8dfaba8394f tuned;
Author
makarius
Browse Repository
No Builds
No Audits
001739cb8d08 clarified signature: more explicit types;
Author
makarius
Browse Repository
No Builds
No Audits
61a1bf9eb0ce clarified data: avoid pointless Morphism.transform;
Author
makarius
Browse Repository
No Builds
No Audits
dbc67f6c501c proper Token.Declaration for internal_declaration;
Author
makarius
Browse Repository
No Builds
No Audits
e5bd9b3c6f0f more standard treatment of morphism context;
Author
makarius
Browse Repository
No Builds
No Audits
a01c3bcf22dd tuned: avoid duplication;
Author
makarius
Browse Repository
No Builds
No Audits
a71bfc551891 more standard treatment of morphism context, but hardly relevant here;
Author
makarius
Browse Repository
No Builds
No Audits
e6343330e8df tuned;
Author
makarius
Browse Repository
No Builds
No Audits
11d6a1e62841 more careful treatment of set_context / reset_context for persistent morphisms;
Author
makarius
Browse Repository
No Builds
No Audits
4e865c45458b clarified transfer / trim_context on persistent Token.source (e.g. attribute…
Author
makarius
Browse Repository
No Builds
No Audits
7c9f290dff55 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
edb195122938 support for context within morphism (for background theory);
Author
makarius
Browse Repository
No Builds
No Audits
5ab5add88922 proper transfer to supported "bundle ... begin unbundle ... end", e.g. see…
Author
makarius
Browse Repository
No Builds
No Audits
b6c886b7184f clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
d555983054f3 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
9de0d3d961d4 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
9439ae944a00 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
904242f46ce1 more accurate Thm.trim_context / Thm.transfer;
Author
makarius
Browse Repository
No Builds
No Audits
2d60172c0ade clarified stored thm: result from notes;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (36)

Path

Size

etc/

src/

FOL/

ex/

Locale_Test/

Locale_Test1.thy

HOL/

Analysis/

Abstract_Topological_Spaces.thy

Abstract_Topology.thy

Abstract_Topology_2.thy

Elementary_Metric_Spaces.thy

Product_Topology.thy

Sum_Topology.thy

Statespace/

Tools/

Lifting/

lifting_info.ML

SMT/

z3_replay_rules.ML

Pure/

Concurrent/

thread_position.ML

unsynchronized.ML

General/

Isar/

local_theory.ML

outer_syntax.ML

proof_display.ML

ML/

PIDE/

System/

isabelle_process.ML

Thy/

Tools/

Haskell/

ZF/

Tools/

inductive_package.ML

rISABELLEab8310c0e6d9

etc/options

Loading...

src/FOL/ex/Locale_Test/Locale_Test1.thy

Loading...

src/HOL/Analysis/Abstract_Topological_Spaces.thy

Loading...

src/HOL/Analysis/Abstract_Topology.thy

Loading...

src/HOL/Analysis/Abstract_Topology_2.thy

Loading...

src/HOL/Analysis/Elementary_Metric_Spaces.thy

Loading...

src/HOL/Analysis/Locally.thy

Loading...

src/HOL/Analysis/Product_Topology.thy

Loading...

src/HOL/Analysis/Starlike.thy

Loading...

src/HOL/Analysis/Sum_Topology.thy

Loading...

src/HOL/Statespace/state_space.ML

Loading...

src/HOL/Tools/Lifting/lifting_info.ML

Loading...

src/HOL/Tools/SMT/z3_replay_rules.ML

Loading...

src/Pure/Concurrent/thread_position.ML

Loading...

src/Pure/Concurrent/unsynchronized.ML

Loading...

src/Pure/General/position.ML

Loading...

src/Pure/General/position.scala

Loading...

src/Pure/Isar/attrib.ML

Loading...

src/Pure/Isar/local_theory.ML

Loading...

src/Pure/Isar/outer_syntax.ML

Loading...

src/Pure/Isar/proof_display.ML

Loading...

src/Pure/Isar/toplevel.ML

Loading...

src/Pure/ML/ml_compiler.ML

Loading...

src/Pure/ML/ml_context.ML

Loading...

src/Pure/ML/ml_env.ML

Loading...

src/Pure/ML/ml_file.ML

Loading...

src/Pure/PIDE/markup.ML

Loading...

src/Pure/PIDE/markup.scala

Loading...

src/Pure/PIDE/session.ML

Loading...

src/Pure/System/isabelle_process.ML

Loading...

src/Pure/Thy/thy_info.ML

Loading...

src/Pure/context.ML

Loading...

src/Pure/thm.ML

Loading...

src/Tools/Haskell/Haskell.thy

Loading...

src/ZF/Tools/induct_tacs.ML

Loading...

src/ZF/Tools/inductive_package.ML

Loading...