Diffusion Isabelle 300537844bb7

merged
300537844bb7
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rISABELLE35439ca0133c: proper setup for rule attribute;
rISABELLEcec875dcc59e: Finally, the abstract metric space development

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE300537844bb7: merged.Thu, May 25, 1:58 PM

Merged Changes

cec875dcc59e Finally, the abstract metric space development
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits

Changes (72)

Path

Size

src/

Doc/

Isar_Ref/

HOL/

Bali/

Boolean_Algebras.thy

Data_Structures/

Decision_Procs/

Commutative_Ring.thy

Conversions.thy

Reflective_Field.thy

Eisbach/

method_closure.ML

HOLCF/

Tools/

Library/

Extended_Nat.thy

Extended_Nonnegative_Real.thy

Multiset_Order.thy

adhoc_overloading.ML

Nominal/

nominal_inductive.ML

nominal_inductive2.ML

Nonstandard_Analysis/

Numeral_Simprocs.thy

Product_Type.thy

Real_Asymp/

exp_log_expression.ML

Statespace/

Tools/

BNF/

bnf_fp_def_sugar.ML

bnf_fp_n2m_sugar.ML

bnf_gfp_grec.ML

bnf_gfp_grec_sugar.ML

bnf_lfp_size.ML

Ctr_Sugar/

Function/

Lifting/

lifting_def_code_dt.ML

lifting_setup.ML

Quotient/

quotient_def.ML

quotient_type.ML

Transfer/

transfer_bnf.ML

inductive_set.ML

semiring_normalizer.ML

Provers/

Pure/

Admin/

isabelle_cronjob.scala

Isar/

generic_target.ML

local_theory.ML

ex/

ZF/

rISABELLE300537844bb7

src/Doc/Isar_Ref/Generic.thy

Loading...

src/HOL/Bali/Eval.thy

Loading...

src/HOL/Bali/Evaln.thy

Loading...

src/HOL/Bali/WellType.thy

Loading...

src/HOL/Boolean_Algebras.thy

Loading...

src/HOL/Data_Structures/Less_False.thy

Loading...

src/HOL/Decision_Procs/Commutative_Ring.thy

Loading...

src/HOL/Decision_Procs/Conversions.thy

Loading...

src/HOL/Decision_Procs/Reflective_Field.thy

Loading...

src/HOL/Eisbach/Tests.thy

Loading...

src/HOL/Eisbach/method_closure.ML

Loading...

src/HOL/Enum.thy

Loading...

src/HOL/Finite_Set.thy

Loading...

src/HOL/Fun.thy

Loading...

src/HOL/Groups.thy

Loading...

src/HOL/HOL.thy

Loading...

src/HOL/HOLCF/Cfun.thy

Loading...

src/HOL/HOLCF/Pcpo.thy

Loading...

src/HOL/HOLCF/Tools/fixrec.ML

Loading...

src/HOL/Library/Extended_Nat.thy

Loading...

src/HOL/Library/Extended_Nonnegative_Real.thy

Loading...

src/HOL/Library/Multiset.thy

Loading...

src/HOL/Library/Multiset_Order.thy

Loading...

src/HOL/Library/adhoc_overloading.ML

Loading...

src/HOL/List.thy

Loading...

src/HOL/Nat.thy

Loading...

src/HOL/Nominal/nominal_inductive.ML

Loading...

src/HOL/Nominal/nominal_inductive2.ML

Loading...

src/HOL/Nonstandard_Analysis/NSA.thy

Loading...

src/HOL/Num.thy

Loading...

src/HOL/Numeral_Simprocs.thy

Loading...

src/HOL/Product_Type.thy

Loading...

src/HOL/Real_Asymp/exp_log_expression.ML

Loading...

src/HOL/Set.thy

Loading...

src/HOL/Statespace/state_space.ML

Loading...

src/HOL/Tools/BNF/bnf_def.ML

Loading...

src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

Loading...

src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

Loading...

src/HOL/Tools/BNF/bnf_gfp_grec.ML

Loading...

src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML

Loading...

src/HOL/Tools/BNF/bnf_lfp_size.ML

Loading...

src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

Loading...

src/HOL/Tools/Function/function.ML

Loading...

src/HOL/Tools/Lifting/lifting_def.ML

Loading...

src/HOL/Tools/Lifting/lifting_def_code_dt.ML

Loading...

src/HOL/Tools/Lifting/lifting_setup.ML

Loading...

src/HOL/Tools/Quotient/quotient_def.ML

Loading...

src/HOL/Tools/Quotient/quotient_type.ML

Loading...

src/HOL/Tools/Transfer/transfer_bnf.ML

Loading...

src/HOL/Tools/functor.ML

Loading...

src/HOL/Tools/inductive.ML

Loading...

src/HOL/Tools/inductive_set.ML

Loading...

src/HOL/Tools/semiring_normalizer.ML

Loading...

src/HOL/Tools/typedef.ML

Loading...

src/Provers/order_tac.ML

Loading...

src/Pure/Admin/isabelle_cronjob.scala

Loading...

src/Pure/Isar/attrib.ML

Loading...

src/Pure/Isar/bundle.ML

Loading...

src/Pure/Isar/code.ML

Loading...

src/Pure/Isar/entity.ML

Loading...

src/Pure/Isar/expression.ML

Loading...

src/Pure/Isar/generic_target.ML

Loading...

src/Pure/Isar/isar_cmd.ML

Loading...

src/Pure/Isar/local_theory.ML

Loading...

src/Pure/Isar/locale.ML

Loading...

src/Pure/Isar/method.ML

Loading...

src/Pure/Isar/spec_rules.ML

Loading...

src/Pure/Isar/token.ML

Loading...

src/Pure/ex/Def.thy

Loading...

src/Pure/simplifier.ML

Loading...

src/ZF/OrdQuant.thy

Loading...

src/ZF/pair.thy

Loading...