Diffusion afp-devel ab90e6e586ca

isabelle update -u cite;
ab90e6e586ca
Actions

Description

isabelle update -u cite;

Details

Provenance

makarius

Authored on

Parents

rAFP3090aa3b36a4: added bibliography to ROOT;

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rAFPab90e6e586ca: isabelle update -u cite;.Jan 16 2023, 1:40 PM

Changes (868)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

thys/

AI_Planning_Languages_Semantics/

Lifschitz_Consistency.thy

AODV/

variants/

a_norreqid/

b_fwdrreps/

c_gtobcast/

d_fwdrreqs/

Abstract-Hoare-Logics/

Proc/

PHoareTotal.thy

Procs/

PsLang.thy

Ackermanns_not_PR/

Primrec.thy

Adaptive_State_Counting/

ASC/

ASC_Suite.thy

ATC/

ATC.thy

FSM/

FSM.thy

Aggregation_Algebras/

Aggregation_Algebras.thy

Linear_Aggregation_Algebras.thy

Matrix_Aggregation_Algebras.thy

Algebraic_Numbers/

Algebraic_Number_Tests.thy

Algebraic_Numbers_Prelim.thy

Real_Algebraic_Numbers.thy

Resultant.thy

Algebraic_VCs/

Domain_Quantale.thy

Amicable_Numbers/

Amicable_Numbers.thy

Amortized_Complexity/

Amortized_Examples.thy

Amortized_Framework0.thy

Pairing_Heap_List1_Analysis.thy

Pairing_Heap_List2_Analysis.thy

Pairing_Heap_Tree_Analysis.thy

Pairing_Heap_Tree_Analysis2.thy

Skew_Heap_Analysis.thy

Splay_Tree_Analysis_Optimal.thy

AnselmGod/

AnselmGod.thy

Applicative_Lifting/

Tree_Relabelling.thy

Approximation_Algorithms/

Architectural_Design_Patterns/

Blackboard.thy

Publisher_Subscriber.thy

Singleton.thy

Arith_Prog_Rel_Primes/

Arith_Prog_Rel_Primes.thy

ArrowImpossibilityGS/

Thys/

Attack_Trees/

Auto2_Imperative_HOL/

Functional/

Partial_Equiv_Rel.thy

Rect_Intersect.thy

Union_Find.thy

Imperative/

Dijkstra_Impl.thy

Indexed_PQueue_Impl.thy

LinkedList.thy

SepAuto.thy

Union_Find_Impl.thy

Automated_Stateful_Protocol_Verification/

PSPSP-Manual/

KeyserverEx.thy

introduction.thy

manual.thy

BD_Security_Compositional/

Composing_Security.thy

Composing_Security_Network.thy

Independent_Secrets.thy

Transporting_Security.thy

Banach_Steinhaus/

Banach_Steinhaus.thy

Banach_Steinhaus_Missing.thy

Belief_Revision/

Bernoulli/

Bicategory/

EquivalenceOfBicategories.thy

InternalAdjunction.thy

Prebicategory.thy

PseudonaturalTransformation.thy

Binomial-Heaps/

BirdKMP/

Blue_Eyes/

Bounded_Deducibility_Security/

BD_Security_Triggers.thy

BD_Security_Unwinding.thy

Compositional_Reasoning.thy

Buildings/

Coxeter.thy

BytecodeLogicJmlTypes/

Cachera.thy

Language.thy

C2KA_DistributedSystems/

C2KA.thy

CKA.thy

Communication_C2KA.thy

Stimuli.thy

CAVA_LTL_Modelchecker/

Nested_DFS/

NDFS_SI.thy

CISC-Kernel/

step/

Step_configuration.thy

Step_vpeq_locally_respects.thy

Step_vpeq_weakly_step_consistent.thy

trace/

Rushby-with-Control/

CISK.thy

K.thy

Separation_kernel_model.thy

CRDT/

CRYSTALS-Kyber/

CSP_RefTK/

CZH_Elementary_Categories/

czh_ecategories/

CZH_DG_CAT.thy

CZH_DG_FUNCT.thy

CZH_ECAT_CSimplicial.thy

CZH_ECAT_Category.thy

CZH_ECAT_Comma.thy

CZH_ECAT_Cone.thy

CZH_ECAT_Discrete.thy

CZH_ECAT_Introduction.thy

CZH_ECAT_NTCF.thy

CZH_ECAT_Order.thy

CZH_ECAT_Ordinal.thy

CZH_ECAT_PCategory.thy

CZH_ECAT_Par.thy

CZH_ECAT_Parallel.thy

CZH_ECAT_Small_Category.thy

CZH_ECAT_Structure_Example.thy

CZH_ECAT_Subcategory.thy

CZH_ECAT_Yoneda.thy

CZH_SMC_FUNCT.thy

CZH_Foundations/

czh_digraphs/

CZH_DG_Small_DGHM.thy

CZH_DG_Small_Digraph.thy

CZH_DG_Subdigraph.thy

CZH_DG_TDGHM.thy

czh_introduction/

CZH_Introduction.thy

czh_semicategories/

CZH_DG_SemiCAT.thy

CZH_SMC_Introduction.thy

CZH_SMC_NTSMCF.thy

CZH_SMC_PSemicategory.thy

CZH_SMC_Rel.thy

CZH_SMC_Semicategory.thy

CZH_SMC_Semifunctor.thy

CZH_SMC_Set.thy

CZH_SMC_Simple.thy

CZH_SMC_Small_Semicategory.thy

CZH_SMC_Subsemicategory.thy

czh_sets/

CZH_Sets_IF.thy

CZH_Sets_Introduction.thy

CZH_Sets_MIF.thy

CZH_Sets_Ordinals.thy

ex/

CZH_EX_Replacement.thy

CZH_EX_TS.thy

CZH_Universal_Constructions/

czh_ucategories/

CZH_UCAT_Adjoints.thy

CZH_UCAT_Comma.thy

CZH_UCAT_Introduction.thy

CZH_UCAT_Kan.thy

CZH_UCAT_Limit.thy

CZH_UCAT_Limit_Equalizer.thy

CZH_UCAT_Limit_IT.thy

CZH_UCAT_Limit_Product.thy

CZH_UCAT_Limit_Pullback.thy

CZH_UCAT_PWKan.thy

CZH_UCAT_PWKan_Example.thy

CZH_UCAT_Pointed.thy

CZH_UCAT_Representable.thy

CZH_UCAT_Universal.thy

Case_Labeling/

Examples/

Catalan_Numbers/

Category3/

Chandy_Lamport/

Distributed_System.thy

Example.thy

Snapshot.thy

Clean/

examples/

SquareRoot_concept.thy

src/

ClockSynchInst/

Closest_Pair_Points/

Closest_Pair_Alternative.thy

CoCon/

Traceback_Properties.thy

CoSMeDis/

API_Network.thy

Post_Confidentiality/

DYNAMIC_Post_ISSUER.thy

DYNAMIC_Post_Value_Setup_ISSUER.thy

Independent_Posts/

Independent_Post_Observation_Setup_ISSUER.thy

Post_ISSUER.thy

Post_Intro.thy

Post_Observation_Setup_ISSUER.thy

Post_Observation_Setup_RECEIVER.thy

Post_RECEIVER.thy

System_Specification.thy

CoSMed/

Post_Confidentiality/

Post.thy

Traceback_Properties/

Traceback_Intro.thy

Collections/

Userguides/

ICF_Userguide.thy

Refine_Monadic_Userguide.thy

Combinable_Wands/

CombinableWands.thy

PosRat.thy

Combinatorics_Words/

CoWBasic.thy

Lyndon_Schutzenberger.thy

Periodicity_Lemma.thy

Submonoids.thy

Combinatorics_Words_Graph_Lemma/

Graph_Lemma.thy

Combinatorics_Words_Lyndon/

Lyndon.thy

Comparison_Sort_Lower_Bound/

Comparison_Sort_Lower_Bound.thy

Complete_Non_Orders/

Binary_Relations.thy

Complete_Relations.thy

Fixed_Points.thy

Kleene_Fixed_Point.thy

Complex_Bounded_Operators/

Cblinfun_Code.thy

Complex_Bounded_Linear_Function.thy

Complex_Inner_Product.thy

Complex_Geometry/

More_Transcendental.thy

Oriented_Circlines.thy

ConcurrentGC/

ConcurrentIMP/

Infinite_Sequences.thy

LTL.thy

ex/

CIMP_one_place_buffer.thy

Concurrent_Ref_Alg/

Galois_Connections.thy

Rely_Quotient.thy

Conditional_Simplification/

CS_Reference.thy

Conditional_Transfer_Rule/

CTR/

UD/

Consensus_Refined/

Containers/

Containers_Userguide.thy

Core_DOM/

common/

Core_DOM_Basic_Datatypes.thy

preliminaries/

Hiding_Type_Variables.thy

Core_SC_DOM/

common/

Core_DOM_Basic_Datatypes.thy

preliminaries/

Hiding_Type_Variables.thy

Cotangent_PFD_Formula/

Cotangent_PFD_Formula.thy

Count_Complex_Roots/

Count_Rectangle.thy

DPRM_Theorem/

Diophantine/

Parametric_Polynomials.thy

Register_Machine/

RegisterMachineSpecification.thy

DataRefinementIBP/

Diagram.thy

Datatype_Order_Generator/

Hash_Generator.thy

Decreasing-Diagrams/

Decreasing_Diagrams.thy

Delta_System_Lemma/

Design_Theory/

Design_Isomorphisms.thy

Design_Operations.thy

Group_Divisible_Designs.thy

Multisets_Extras.thy

Resolvable_Designs.thy

Dict_Construction/

Documentation/

Introduction.thy

Differential_Game_Logic/

Differential_Game_Logic.thy

Digit_Expansions/

Binary_Operations.thy

Bits_Digits.thy

Dijkstra_Shortest_Path/

Introduction.thy

Diophantine_Eqns_Lin_Hom/

Linear_Diophantine_Equations.thy

Dirichlet_L/

Dirichlet_L_Functions.thy

Dirichlet_Theorem.thy

Dominance_CHK/

Cfg.thy

Dom_Kildall.thy

Sorted_List_Operations2.thy

DynamicArchitectures/

Configuration_Traces.thy

Dynamic_Architecture_Calculus.thy

Efficient-Mergesort/

Efficient_Sort.thy

Elliptic_Curves_Group_Law/

Elliptic_Test.thy

Equivalence_Relation_Enumeration/

Equivalence_Relation_Enumeration.thy

Ergodic_Theory/

Gouezel_Karlsson.thy

Normalizing_Sequences.thy

Euler_MacLaurin/

Euler_MacLaurin.thy

Example-Submission/

Submission.thy

Extended_Finite_State_Machine_Inference/

heuristics/

PTA_Generalisation.thy

Weak_Subsumption.thy

Extended_Finite_State_Machines/

examples/

FLP/

Farkas/

Featherweight_OCL/

examples/

Employee_Model/

Analysis/

Design/

Finger-Trees/

Finite_Fields/

Card_Irreducible_Polynomials.thy

Card_Irreducible_Polynomials_Aux.thy

Finite_Fields_Preliminary_Results.thy

Ring_Characteristic.thy

Finitely_Generated_Abelian_Groups/

Finitely_Generated_Abelian_Groups.thy

First_Order_Terms/

Term.thy

First_Welfare_Theorem/

Preferences.thy

Fishers_Inequality/

Dual_Systems.thy

Fishers_Inequality.thy

Fishers_Inequality_Variations.thy

Incidence_Matrices.thy

Linear_Bound_Argument.thy

Rank_Argument_General.thy

Flow_Networks/

Augmenting_Flow.thy

Ford_Fulkerson.thy

Floyd_Warshall/

Floyd_Warshall.thy

Formal_Puiseux_Series/

FPS_Hensel.thy

Formal_Puiseux_Series.thy

Puiseux_Polynomial_Library.thy

Formal_SSA/

Minimality.thy

Foundation_of_geometry/

Incidence.thy

Frequency_Moments/

Frequency_Moment_0.thy

Frequency_Moment_2.thy

Frequency_Moment_k.thy

FunWithFunctions/

FunWithFunctions.thy

Furstenberg_Topology/

Furstenberg_Topology.thy

Gabow_SCC/

Gabow_SCC.thy

Gabow_Skeleton.thy

Game_Based_Crypto/

CryptHOL_Tutorial.thy

Gauss_Jordan/

Code_Generation_IArrays.thy

Gaussian_Integers/

Gaussian_Integers_Pythagorean_Triples.thy

Generalized_Counting_Sort/

GewirthPGCProof/

GoedelGod/

Goedel_Incompleteness/

Abstract_Representability.thy

Jeroslow_Simplified.thy

Graph_Theory/

Groebner_Bases/

Groebner_Macaulay/

Groebner_Macaulay.thy

Gromov_Hyperbolicity/

Bonk_Schramm_Extension.thy

Gromov_Hyperbolicity.thy

Isometries.thy

Morse_Gromov_Theorem.thy

HOL-CSP/

Conclusion.thy

Introduction.thy

Process.thy

HOLCF-Prelude/

examples/

GHC_Rewrite_Rules.thy

Hales_Jewett/

Heard_Of/

ate/

eigbyz/

lastvoting/

otr/

ute/

uv/

Hermite_Lindemann/

Hermite_Lindemann.thy

Hidden_Markov_Models/

HMM_Example.thy

Higher_Order_Terms/

Fresh_Monad.thy

Lambda_Free_Compat.thy

HotelKeyCards/

Huffman/

Hybrid_Multi_Lane_Spatial_Logic/

perfect/

regular/

Hybrid_Systems_VCs/

Hyperdual/

AnalyticTestFunction.thy

IFC_Tracking/

IMP2_Binary_Heap/

IMP_Compiler/

IMP_Compiler_Reuse/

Incredible_Proof_Machine/

Incredible_Deduction.thy

Inductive_Inference/

CONS_LIM.thy

CP_FIN_NUM.thy

Inductive_Inference_Basics.thy

LIM_BC.thy

Partial_Recursive.thy

Standard_Results.thy

TOTAL_CONS.thy

InformationFlowSlicing/

LiftingIntra.thy

NonInterferenceIntra.thy

InformationFlowSlicing_Inter/

LiftingInter.thy

NonInterferenceInter.thy

Integration/

Interpolation_Polynomials_HOL_Algebra/

Bounded_Degree_Polynomials.thy

Interpolation_Polynomial_Cardinalities.thy

Interval_Arithmetic_Word32/

Interval_Word32.thy

Intro_Dest_Elim/

IDE_Reference.thy

Isabelle_C/

C11-FrontEnd/

appendices/

C_Appendices.thy

examples/

C_paper.thy

src/

C_Ast.thy

Jacobson_Basic_Algebra/

Set_Theory.thy

JinjaThreads/

Examples/

ApprenticeChallenge.thy

JiveDataStoreModel/

Isabelle_Store/

Location.thy

Store.thy

StoreProperties.thy

Jordan_Normal_Form/

Jordan_Normal_Form_Existence.thy

Matrix_IArray_Impl.thy

KAD/

Antidomain_Semiring.thy

Domain_Semiring.thy

Modal_Kleene_Algebra.thy

Modal_Kleene_Algebra_Applications.thy

KAT_and_DRA/

SingleSorted/

KBPs/

KD_Tree/

Kleene_Algebra/

Kleene_Algebra_Models.thy

Matrix.thy

Omega_Algebra.thy

Omega_Algebra_Models.thy

Knights_Tour/

KnightsTour.thy

Knuth_Morris_Pratt/

KMP.thy

Kuratowski_Closure_Complement/

KuratowskiClosureComplementTheorem.thy

LLL_Basis_Reduction/

Gram_Schmidt_Int.thy

LLL_Factorization/

Factorization_Algorithm_16_22.thy

LOFT/

OpenFlow_Documentation.thy

LTL/

Rewriting.thy

Lam-ml-Normalization/

LambdaAuth/

LambdaMu/

Laplace_Transform/

Laplace_Transform_Library.thy

LatticeProperties/

Lattice_Ordered_Group.thy

Modular_Distrib_Lattice.thy

Launchbury/

CorrectnessOriginal.thy

Denotational.thy

EverythingAdequacy.thy

Launchbury.thy

ValueSimilarity.thy

Laws_of_Large_Numbers/

Laws_of_Large_Numbers.thy

Lehmer/

Lehmer.thy

Lifting_Definition_Option/

Lifting_Definition_Option_Examples.thy

LinearQuantifierElim/

Thys/

Liouville_Numbers/

Liouville_Numbers.thy

List_Interleaving/

ListInterleaving.thy

List_Update/

Move_to_Front.thy

Logging_Independent_Anonymity/

Anonymity.thy

Definitions.thy

Lowe_Ontological_Argument/

LoweOntologicalArgument_1.thy

Lucas_Theorem/

MFMC_Countable/

Matrix_For_Marginals.thy

Rel_PMF_Characterisation_MFMC.thy

MFOTL_Monitor/

Mason_Stothers/

Max-Card-Matching/

Median_Method/

Menger/

Mereology/

Mersenne_Primes/

Minimal_SSA/

Minsky_Machines/

Recursive_Inseparability.thy

Monad_Memo_DP/

example/

Bellman_Ford.thy

Knapsack.thy

Monad_Normalisation/

Monad_Normalisation.thy

MonoidalCategory/

MonoidalCategory.thy

MonoidalFunctor.thy

MuchAdoAboutTwo/

MuchAdoAboutTwo.thy

Multi_Party_Computation/

Multirelations/

Multiset_Ordering_NPC/

Multiset_Ordering_NP_Hard.thy

Multiset_Ordering_in_NP.thy

RPO_NP_Hard.thy

Myhill-Nerode/

Myhill.thy

Native_Word/

Uint_Userguide.thy

Network_Security_Policy_Verification/

TopoS_Interface.thy

TopoS_Stateful_Policy.thy

Noninterference_CSP/

CSPNoninterference.thy

ClassicalNoninterference.thy

GeneralizedNoninterference.thy

Noninterference_Concurrent_Composition/

ConcurrentComposition.thy

Noninterference_Generic_Unwinding/

GenericUnwinding.thy

Noninterference_Inductive_Unwinding/

InductiveUnwinding.thy

Noninterference_Ipurge_Unwinding/

DeterministicProcesses.thy

IpurgeUnwinding.thy

Noninterference_Sequential_Composition/

Counterexamples.thy

Propaedeutics.thy

SequentialComposition.thy

OpSets/

Optics/

Optimal_BST/

Orbit_Stabiliser/

Order_Lattice_Props/

Closure_Operators.thy

Galois_Connections.thy

Order_Duality.thy

Order_Lattice_Props.thy

Order_Lattice_Props_Wenzel.thy

Ordinary_Differential_Equations/

Ex/

Examples_One_Step_Method.thy

Examples_Poincare_Map.thy

IVP/

Upper_Lower_Solution.thy

PAC_Checker/

PAL/

PCF/

Logical_Relations.thy

PLM/

POPLmark-deBruijn/

Package_logic/

Padic_Field/

Padic_Field_Polynomials.thy

Padic_Field_Powers.thy

Padic_Fields.thy

Padic_Semialgebraic_Function_Ring.thy

Padic_Ints/

Extended_Int.thy

Hensels_Lemma.thy

Padic_Construction.thy

Padic_Int_Topology.thy

Padic_Integers.thy

Pairing_Heap/

Pairing_Heap_List1.thy

Pairing_Heap_List2.thy

Pairing_Heap_Tree.thy

Password_Authentication_Protocol/

Propaedeutics.thy

Pell/

Efficient_Discrete_Sqrt.thy

Pell.thy

Perron_Frobenius/

Perron_Frobenius.thy

Spectral_Radius_Theory.thy

Pi_Transcendental/

Pi_Transcendental.thy

Poincare_Disc/

Hyperbolic_Functions.thy

Tarski.thy

Polynomial_Factorization/

Prime_Factorization.thy

Polynomials/

Pop_Refinement/

Posix-Lexing/

Extensions/

Derivatives3.thy

Power_Sum_Polynomials/

Power_Sum_Polynomials.thy

Power_Sum_Puzzle.thy

Pratt_Certificate/

Pratt_Certificate.thy

Prefix_Free_Code_Combinators/

Prefix_Free_Code_Combinators.thy

Prim_Dijkstra_Simple/

Chapter_Dijkstra.thy

Chapter_Prim.thy

Prime_Distribution_Elementary/

PNT_Consequences.thy

Prime_Number_Theorem/

Newman_Ingham_Tauberian.thy

Prime_Counting_Functions.thy

Priority_Queue_Braun/

Priority_Queue_Braun.thy

Probabilistic_Prime_Tests/

Carmichael_Numbers.thy

Probabilistic_While/

Program-Conflict-Analysis/

AcquisitionHistory.thy

Flowgraph.thy

Projective_Geometry/

Higher_Projective_Space_Rank_Axioms.thy

Propositional_Proof_Systems/

ND_Compl_Truthtable.thy

Quantales/

Quantic_Nuclei_Conuclei.thy

Quasi_Borel_Spaces/

Bayesian_Linear_Regression.thy

Binary_Product_QuasiBorel.thy

Measure_as_QuasiBorel_Measure.thy

Pair_QuasiBorel_Measure.thy

Product_QuasiBorel.thy

QuasiBorel.thy

StandardBorel.thy

Quick_Sort_Cost/

Quick_Sort_Average_Case.thy

Randomised_Quick_Sort.thy

ROBDD/

BDT.thy

Random_BSTs/

Random_BSTs.thy

Rank_Nullity_Theorem/

Recursion-Theory-I/

Refine_Monadic/

RefinementReactive/

Registers/

Axioms_Complement_Quantum.thy

Regular-Sets/

Derivatives.thy

Regular_Algebras/

Pratts_Counterexamples.thy

Regular_Algebras.thy

Relational-Incorrectness-Logic/

RelationalIncorrectness.thy

Relational_Disjoint_Set_Forests/

Disjoint_Set_Forests.thy

Relational_Forests/

Algorithms.thy

Relational_Method/

Definitions.thy

Relational_Minimum_Spanning_Trees/

Kruskal.thy

Prim.thy

Relational_Paths/

More_Relation_Algebra.thy

Path_Algorithms.thy

Paths.thy

ResiduatedTransitionSystem/

LambdaCalculus.thy

Residuated_Lattices/

Action_Algebra.thy

Roy_Floyd_Warshall/

Roy_Floyd_Warshall.thy

SATSolverVerification/

KrsticGoel.thy

NieuwenhuisOliverasTinelli.thy

SatSolverVerification.thy

SCC_Bloemen_Sequential/

SCC_Bloemen_Sequential.thy

SIFPL/

Safe_Range_RC/

Schutz_Spacetime/

TemporalOrderOnPath.thy

SenSocialChoice/

Separation_Logic_Unbounded/

AutomaticVerifiers.thy

SequentInvertibility/

SRCTransforms.thy

Shivers-CFA/

CPSScheme.thy

ShortestPath/

ShortestPath.thy

Sigma_Commit_Crypto/

Chaum_Pedersen_Sigma_Commit.thy

Commitment_Schemes.thy

Pedersen.thy

Rivest.thy

Schnorr_Sigma_Commit.thy

Sigma_Protocols.thy

Simpl/

AlternativeSmallStep.thy

UserGuide.thy

Simplex/

Abstract_Linear_Poly.thy

Simplex.thy

Simplicial_complexes_and_boolean_functions/

Binary_operations.thy

Boolean_functions.thy

Evasive.thy

Simplicial_complex.thy

SimplifiedOntologicalArgument/

BaseDefs.thy

HOML.thy

KanckosLethenNo2Possibilist.thy

SimpleVariantSEinT.thy

SimplifiedOntologicalArgument.thy

UFilterVariant.thy

Skew_Heap/

Skew_Heap.thy

Sliding_Window_Algorithm/

Sophomores_Dream/

Splay_Tree/

Sqrt_Babylonian/

Stable_Matching/

Stellar_Quorums/

Stern_Brocot/

Stern_Brocot_Tree.thy

Stirling_Formula/

Gamma_Asymptotics.thy

Stone_Algebras/

Filters.thy

P_Algebras.thy

Stone_Construction.thy

Stone_Kleene_Relation_Algebras/

Iterings.thy

Kleene_Algebras.thy

Kleene_Relation_Algebras.thy

Matrix_Kleene_Algebras.thy

Stone_Relation_Algebras/

Fixpoints.thy

Matrix_Relation_Algebras.thy

Relation_Algebras.thy

Semirings.thy

Store_Buffer_Reduction/

Preliminaries.thy

Text.thy

Stream_Fusion_Code/

Stream_Fusion_Examples.thy

Stream_Fusion_LList.thy

Stream_Fusion_List.thy

Stuttering_Equivalence/

isabelle update -u cite;ab90e6e586caActions

Description

Details

Event Timeline

Changes (868)Show All Changes

Very Large Commit

isabelle update -u cite;
ab90e6e586ca
Actions

Changes (868)
Show All Changes