Diffusion afp-devel 0e249fc28c65

merge
0e249fc28c65
Actions

Tags

None

Subscribers

None

Description

merge

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFPaf435c34b495: new entries by Mihails Milehins
rAFPd278a335ac39: eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib"

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP0e249fc28c65: merge.Sep 30 2021, 2:30 PM

Merged Changes

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

d278a335ac39 eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib"
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
1ab5075701b4 repaired slip
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f5b9195ac412 feat(SpecCheck) folder renaming, types for tests
Author
kappelmann
Browse Repository
No Builds
No Audits
e632b4a6d1d4 tuned
Author
nipkow
Browse Repository
No Builds
No Audits
2056abab0dd6 mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"…
Author
makarius
Browse Repository
No Builds
No Audits
61b65f5bfdbe ported Design-Theory from AFP 2021 to devel
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
d724a03eef28 ported Three-Circles from AFP 2021 to devel
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
fbfac64da6d5 move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
6929ff388470 ported Cubic_Quartic_Equations from AFP 2021 to devel
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
983817c24bc0 merge of AFP 2021
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
194bd67c97ea clarified modules, according to Isabelle/534b231ce041;
Author
makarius
Browse Repository
No Builds
No Audits
d12a1ce2753f bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.
Author
makarius
Browse Repository
No Builds
No Audits
3206db92e73b clarified signature, according to Isabelle/d882abae3379;
Author
makarius
Browse Repository
No Builds
No Audits
33b9d9a97696 explicit predicate for confined bit range avoids cyclic rewriting in presence…
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a168f8f2bbc3 tuned signature, according to Isabelle/28a582aa25dd;
Author
makarius
Browse Repository
No Builds
No Audits
cb975509a607 eliminated Specification.definition', following Isabelle/6876e3d5e362;
Author
makarius
Browse Repository
No Builds
No Audits
72c37b1f419b clarified signature: more scalable operations, according to…
Author
makarius
Browse Repository
No Builds
No Audits
a265f0b030f3 clarified signature, according to Isabelle/612b7e0d6721;
Author
makarius
Browse Repository
No Builds
No Audits
0608aee85535 tuned signature, according to Isabelle/839a6e284545;
Author
makarius
Browse Repository
No Builds
No Audits
e58cb507f0b7 merged
Author
sterraf
Browse Repository
No Builds
No Audits
dfc972b8491c Backed out changeset ef19e4e58b8c
Author
sterraf
Browse Repository
No Builds
No Audits
301f0280d6c6 avoid hardwired document;
Author
makarius
Browse Repository
No Builds
No Audits
4ed6e19f5983 merged
Author
makarius
Browse Repository
No Builds
No Audits
9a1fa4cf1287 tuned signature, according to Isabelle/9d9e7ed01dbb;
Author
makarius
Browse Repository
No Builds
No Audits
723c9dd87715 clarified signature, according to Isabelle/9d9e7ed01dbb;
Author
makarius
Browse Repository
No Builds
No Audits
33062a15318c clarified signature, according to Isabelle/9d9e7ed01dbb;
Author
makarius
Browse Repository
No Builds
No Audits
5a2b8f5e016e clarified signature, according to Isabelle/9d9e7ed01dbb;
Author
makarius
Browse Repository
No Builds
No Audits
ce490469c76e simplified, using Isabelle/ML operations;
Author
makarius
Browse Repository
No Builds
No Audits
a815068160f3 adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for…
Author
makarius
Browse Repository
No Builds
No Audits
af371b9b111d tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
9a6a94253c8d more scalable operations;
Author
makarius
Browse Repository
No Builds
No Audits
f949f8939459 merged
Author
sterraf
Browse Repository
No Builds
No Audits
ef19e4e58b8c synthesized formulas have their variables permuted
Author
sterraf
Browse Repository
No Builds
No Audits
76b26779f90c merged
Author
paulson
Browse Repository
No Builds
No Audits
4e16e45730a4 fixes for cardinality lemmas
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
34eccbb60a01 proper inst table;
Author
makarius
Browse Repository
No Builds
No Audits
80d141ead0ab Graphic rendering of Relational_Method PDF files refined.
Author
Pasquale Noce <pasquale.noce@hidglobal.com>
Browse Repository
No Builds
No Audits
5fa903cd1a85 Entry Relational_Method updated.
Author
Pasquale Noce <pasquale.noce@hidglobal.com>
Browse Repository
No Builds
No Audits
0320f17157ee more realistic timeout;
Author
makarius
Browse Repository
No Builds
No Audits
d5bc84fd503c clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
f1bf23e16821 follow Isabelle/53e28c438f96;
Author
makarius
Browse Repository
No Builds
No Audits
e3caeb84ccd9 clarified signature, following Isabelle/a3b0fc510705;
Author
makarius
Browse Repository
No Builds
No Audits
7bd41cfb12ad merged
Author
nipkow
Browse Repository
No Builds
No Audits
376d3a9f6285 tuned
Author
nipkow
Browse Repository
No Builds
No Audits
897dc683c2ec consolidation of rules for bit operations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
dd34e0937e25 tuned name
Author
nipkow
Browse Repository
No Builds
No Audits
6feef30fcece Fix typo
Author
Thomas Bauereiss <thomas@bauereiss.name>
Browse Repository
No Builds
No Audits
b31669de2911 Tune references
Author
Thomas Bauereiss <thomas@bauereiss.name>
Browse Repository
No Builds
No Audits
717cfc6afe61 Remove redundant license
Author
Thomas Bauereiss <thomas@bauereiss.name>
Browse Repository
No Builds
No Audits
1ac7f6375fda more realistic timeout: approx. 5min CPU time;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (376)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

CZH_Elementary_Categories

czh_ecategories

CZH_DG_FUNCT.thy

CZH_ECAT_CAT.thy

CZH_ECAT_CSimplicial.thy

CZH_ECAT_Category.thy

CZH_ECAT_Comma.thy

CZH_ECAT_Conclusions.thy

CZH_ECAT_Discrete.thy

CZH_ECAT_FUNCT.thy

CZH_ECAT_Functor.thy

CZH_ECAT_GRPH.thy

CZH_ECAT_Hom.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_Rel.thy

CZH_ECAT_SS.thy

CZH_ECAT_SemiCAT.thy

CZH_ECAT_Set.thy

CZH_ECAT_Simple.thy

CZH_ECAT_Small_Category.thy

CZH_ECAT_Small_Functor.thy

CZH_ECAT_Small_NTCF.thy

CZH_ECAT_Small_Order.thy

CZH_ECAT_Structure_Example.thy

CZH_ECAT_Subcategory.thy

CZH_ECAT_Yoneda.thy

CZH_SMC_CAT.thy

CZH_SMC_FUNCT.thy

CZH_Foundations

CZH_DG_Conclusions.thy

CZH_DG_DGHM.thy

CZH_DG_Digraph.thy

CZH_DG_GRPH.thy

CZH_DG_Introduction.thy

CZH_DG_PDigraph.thy

CZH_DG_Simple.thy

CZH_DG_Small_DGHM.thy

CZH_DG_Small_Digraph.thy

CZH_DG_Small_TDGHM.thy

CZH_DG_Subdigraph.thy

CZH_DG_TDGHM.thy

czh_introduction

CZH_Introduction.thy

czh_semicategories

CZH_DG_SemiCAT.thy

CZH_SMC_Conclusions.thy

CZH_SMC_GRPH.thy

CZH_SMC_Introduction.thy

CZH_SMC_NTSMCF.thy

CZH_SMC_PSemicategory.thy

CZH_SMC_Par.thy

CZH_SMC_Rel.thy

CZH_SMC_SemiCAT.thy

CZH_SMC_Semicategory.thy

CZH_SMC_Semifunctor.thy

CZH_SMC_Set.thy

CZH_SMC_Simple.thy

CZH_SMC_Small_NTSMCF.thy

CZH_SMC_Small_Semicategory.thy

CZH_SMC_Small_Semifunctor.thy

CZH_SMC_Subsemicategory.thy

CZH_Sets_BRelations.thy

CZH_Sets_Cardinality.thy

CZH_Sets_Conclusions.thy

CZH_Sets_Equipollence.thy

CZH_Sets_FBRelations.thy

CZH_Sets_FSequences.thy

CZH_Sets_IF.thy

CZH_Sets_Introduction.thy

CZH_Sets_MIF.thy

CZH_Sets_NOP.thy

CZH_Sets_Nat.thy

CZH_Sets_Ordinals.thy

CZH_Sets_Sets.thy

CZH_Sets_VNHS.thy

CZH_Sets_ZQR.thy

CZH_Utilities.thy

HOL_CContinuum.thy

CZH_EX_Algebra.thy

CZH_EX_Replacement.thy

CZH_Universal_Constructions

czh_ucategories

CZH_UCAT_Adjoints.thy

CZH_UCAT_Complete.thy

CZH_UCAT_Conclusions.thy

CZH_UCAT_Introduction.thy

CZH_UCAT_Kan.thy

CZH_UCAT_Limit.thy

CZH_UCAT_PWKan.thy

CZH_UCAT_PWKan_Example.thy

CZH_UCAT_Universal.thy

Conditional_Simplification

CS_Cond_Simp.ML

CS_Reference.thy

More_Tactical.ML

Reference_Prerequisites.thy

Conditional_Transfer_Rule

CTR_Algorithm.ML

CTR_Conversions.ML

CTR_Foundations.ML

CTR_Parametricity.ML

CTR_Postprocessing.ML

CTR_Reference.thy

CTR_Relativization.ML

CTR_Relators.ML

CTR_TEST_PROCESS_CTR_RELATOR.ML

CTR_TEST_PROCESS_RELATIVIZATION.ML

CTR_Introduction.thy

CTR_Utilities.ML

More_Binding.ML

More_HOLogic.ML

More_Library.ML

More_Simplifier.ML

More_Transfer.ML

More_Variable.ML

UT_Test_Suite.ML

Reference_Prerequisites.thy

UD_TEST_UNOVERLOAD_DEFINITION.ML

UD_Reference.thy

Dom_Kildall.thy

Dom_Kildall_Correct.thy

Dom_Kildall_Property.thy

Dom_Semi_List.thy

Sorted_Less2.thy

Sorted_List_Operations2.thy

Intro_Dest_Elim

IDE_Reference.thy

IDE_Utilities.ML

Reference_Prerequisites.thy

Logging_Independent_Anonymity

Definitions.thy

Possibility.thy

Schutz_Spacetime

TemporalOrderOnPath.thy

TernaryOrdering.thy

Types_To_Sets_Extension

ETTS_Algorithm.ML

ETTS_Auxiliary.thy

ETTS_Context.ML

ETTS_Substitution.ML

ETTS_Tactics.ML

More_HOLogic.ML

More_Library.ML

More_Simplifier.ML

More_Tactical.ML

More_Transfer.ML

ETTS_Utilities.ML

ETTS_Examples.thy

ETTS_Introduction.thy

ETTS_Syntax.thy

ETTS_Theory.thy

Manual_Prerequisites.thy

ETTS_TEST_AMEND_CTXT_DATA.ML

ETTS_TEST_TTS_ALGORITHM.ML

ETTS_TEST_TTS_REGISTER_SBTS.ML

Introduction.thy

SML_Relativization

SML_Monoids.thy

SML_Semigroups.thy

SML_Semirings.thy

Lifting_Set_Ext.thy

Product_Type_Ext.thy

SML_Relations.thy

Transfer_Ext.thy

SML_Complete_Lattices.thy

SML_Lattices.thy

SML_Linorders.thy

SML_Semilattices.thy

SML_Conclusions.thy

SML_Introduction.thy

SML_Simple_Orders.thy

SML_Ordered_Topological_Spaces.thy

SML_Product_Topology.thy

SML_Topological_Space.thy

SML_Topological_Space_Countability.thy

TTS_Foundations

Set_Semigroups.thy

Type_Semigroups.thy

FNDS_Conclusions.thy

FNDS_Introduction.thy

FNDS_Auxiliary.thy

FNDS_Definite_Description.thy

FNDS_Lifting_Set_Ext.thy

FNDS_Set_Ext.thy

Set_Simple_Orders.thy

Type_Simple_Orders.thy

VS_Conclusions.thy

VS_Prerequisites.thy

VS_Vector_Spaces.thy

Abstract-Rewriting.html

Berlekamp_Zassenhaus.html

CZH_Elementary_Categories.html

CZH_Foundations.html

CZH_Universal_Constructions.html

Conditional_Simplification.html

Conditional_Transfer_Rule.html

Containers.html

Cubic_Quartic_Equations.html

Dominance_CHK.html

Efficient-Mergesort.html

Gauss_Jordan.html

Hermite_Lindemann.html

Intro_Dest_Elim.html

Logging_Independent_Anonymity.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Schutz_Spacetime.html

Subresultants.html

Types_To_Sets_Extension.html

VectorSpace.html

ZFC_in_HOL.html

statistics.html

rAFP0e249fc28c65

metadata/metadata

thys/CZH_Elementary_Categories/LICENSE

thys/CZH_Elementary_Categories/ROOT

thys/CZH_Elementary_Categories/czh_ecategories/CZH_DG_CAT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_DG_FUNCT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_CAT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_CSimplicial.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Category.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Comma.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Conclusions.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Discrete.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_FUNCT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Functor.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_GRPH.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Hom.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Introduction.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_NTCF.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Order.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Ordinal.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_PCategory.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Par.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Parallel.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Rel.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_SS.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_SemiCAT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Set.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Simple.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Category.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Functor.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_NTCF.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Order.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Structure_Example.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Subcategory.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Yoneda.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_SMC_CAT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_SMC_FUNCT.thy

thys/CZH_Elementary_Categories/document/extra.sty

thys/CZH_Elementary_Categories/document/iman.sty

thys/CZH_Elementary_Categories/document/isar.sty

thys/CZH_Elementary_Categories/document/root.bib

thys/CZH_Elementary_Categories/document/root.tex

thys/CZH_Elementary_Categories/document/style.sty

thys/CZH_Foundations/LICENSE

thys/CZH_Foundations/ROOT

thys/CZH_Foundations/czh_digraphs/CZH_DG_Conclusions.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_DGHM.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Digraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_GRPH.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Introduction.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_PDigraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Par.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Rel.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Set.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Simple.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_DGHM.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_Digraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_TDGHM.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Subdigraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_TDGHM.thy

thys/CZH_Foundations/czh_introduction/CZH_Introduction.thy

thys/CZH_Foundations/czh_semicategories/CZH_DG_SemiCAT.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Conclusions.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_GRPH.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Introduction.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_NTSMCF.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_PSemicategory.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Par.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Rel.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_SemiCAT.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semicategory.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semifunctor.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Set.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Simple.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_NTSMCF.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_Semicategory.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_Semifunctor.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Subsemicategory.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_BRelations.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Cardinality.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Conclusions.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Equipollence.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_FBRelations.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_FSequences.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_IF.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Introduction.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_MIF.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_NOP.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Nat.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Ordinals.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Sets.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_VNHS.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_ZQR.thy

thys/CZH_Foundations/czh_sets/CZH_Utilities.thy

thys/CZH_Foundations/czh_sets/HOL_CContinuum.thy

thys/CZH_Foundations/czh_sets/ex/CZH_EX_Algebra.thy

thys/CZH_Foundations/czh_sets/ex/CZH_EX_Replacement.thy

thys/CZH_Foundations/czh_sets/ex/CZH_EX_TS.thy

thys/CZH_Foundations/document/extra.sty

thys/CZH_Foundations/document/iman.sty

thys/CZH_Foundations/document/isar.sty

thys/CZH_Foundations/document/root.bib

thys/CZH_Foundations/document/root.tex

thys/CZH_Foundations/document/style.sty

thys/CZH_Universal_Constructions/LICENSE

thys/CZH_Universal_Constructions/ROOT

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Adjoints.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Complete.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Conclusions.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Introduction.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Kan.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan_Example.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Universal.thy

thys/CZH_Universal_Constructions/document/extra.sty

thys/CZH_Universal_Constructions/document/iman.sty

thys/CZH_Universal_Constructions/document/isar.sty

thys/CZH_Universal_Constructions/document/root.bib

thys/CZH_Universal_Constructions/document/root.tex

thys/CZH_Universal_Constructions/document/style.sty

thys/Conditional_Simplification/CS_Cond_Simp.ML

thys/Conditional_Simplification/CS_Reference.thy

thys/Conditional_Simplification/CS_TimeIt.ML

thys/Conditional_Simplification/CS_Tools/CS_Stats.ML

thys/Conditional_Simplification/CS_Tools/CS_Tools.thy

thys/Conditional_Simplification/CS_Tools/More_Tactical.ML

thys/Conditional_Simplification/CS_UM.ML

thys/Conditional_Simplification/IHOL_CS.thy

thys/Conditional_Simplification/LICENSE

thys/Conditional_Simplification/ROOT

thys/Conditional_Simplification/Reference_Prerequisites.thy

thys/Conditional_Simplification/document/extra.sty

thys/Conditional_Simplification/document/iman.sty

thys/Conditional_Simplification/document/isar.sty

thys/Conditional_Simplification/document/root.bib

thys/Conditional_Simplification/document/root.tex

thys/Conditional_Transfer_Rule/CTR/CTR.ML

thys/Conditional_Transfer_Rule/CTR/CTR.thy

thys/Conditional_Transfer_Rule/CTR/CTR_Algorithm.ML

thys/Conditional_Transfer_Rule/CTR/CTR_Conversions.ML

thys/Conditional_Transfer_Rule/CTR/CTR_Foundations.ML

thys/Conditional_Transfer_Rule/CTR/CTR_Parametricity.ML

thys/Conditional_Transfer_Rule/CTR/CTR_Postprocessing.ML

thys/Conditional_Transfer_Rule/CTR/CTR_Reference.thy

thys/Conditional_Transfer_Rule/CTR/CTR_Relativization.ML

thys/Conditional_Transfer_Rule/CTR/CTR_Relators.ML

thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_CTR_RELATOR.ML

thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_RELATIVIZATION.ML

thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy

thys/Conditional_Transfer_Rule/CTR_Introduction.thy

thys/Conditional_Transfer_Rule/CTR_Tools/CTR_Tools.thy

thys/Conditional_Transfer_Rule/CTR_Tools/CTR_Utilities.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Binding.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_HOLogic.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Library.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Logic.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Simplifier.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Sort.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Term.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Thm.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Transfer.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Type.ML

thys/Conditional_Transfer_Rule/CTR_Tools/More_Variable.ML

thys/Conditional_Transfer_Rule/IML_UT/IML_UT.thy

thys/Conditional_Transfer_Rule/IML_UT/UT_Test_Suite.ML

thys/Conditional_Transfer_Rule/LICENSE

thys/Conditional_Transfer_Rule/ROOT

thys/Conditional_Transfer_Rule/Reference_Prerequisites.thy

thys/Conditional_Transfer_Rule/UD/Tests/UD_TEST_UNOVERLOAD_DEFINITION.ML

thys/Conditional_Transfer_Rule/UD/Tests/UD_Tests.thy

thys/Conditional_Transfer_Rule/UD/UD.ML

thys/Conditional_Transfer_Rule/UD/UD.thy

thys/Conditional_Transfer_Rule/UD/UD_Consts.ML

thys/Conditional_Transfer_Rule/UD/UD_Reference.thy

thys/Conditional_Transfer_Rule/UD/UD_With.ML

thys/Conditional_Transfer_Rule/document/extra.sty

thys/Conditional_Transfer_Rule/document/iman.sty

thys/Conditional_Transfer_Rule/document/isar.sty

thys/Conditional_Transfer_Rule/document/root.bib

thys/Conditional_Transfer_Rule/document/root.tex

thys/Dominance_CHK/Cfg.thy

thys/Dominance_CHK/Dom_Kildall.thy

thys/Dominance_CHK/Dom_Kildall_Correct.thy

thys/Dominance_CHK/Dom_Kildall_Property.thy

thys/Dominance_CHK/Dom_Semi_List.thy

thys/Dominance_CHK/Listn.thy

thys/Dominance_CHK/ROOT

thys/Dominance_CHK/Semilat.thy

thys/Dominance_CHK/Sorted_Less2.thy

thys/Dominance_CHK/Sorted_List_Operations2.thy

thys/Dominance_CHK/document/root.bib

thys/Dominance_CHK/document/root.tex

thys/Intro_Dest_Elim/IDE.ML

thys/Intro_Dest_Elim/IDE_Reference.thy

thys/Intro_Dest_Elim/IDE_Tools/IDE_Tools.thy

thys/Intro_Dest_Elim/IDE_Tools/IDE_Utilities.ML

thys/Intro_Dest_Elim/IHOL_IDE.thy

thys/Intro_Dest_Elim/LICENSE

thys/Intro_Dest_Elim/ROOT

thys/Intro_Dest_Elim/Reference_Prerequisites.thy

thys/Intro_Dest_Elim/document/extra.sty

thys/Intro_Dest_Elim/document/iman.sty

thys/Intro_Dest_Elim/document/isar.sty

thys/Intro_Dest_Elim/document/root.bib

thys/Intro_Dest_Elim/document/root.tex

thys/Logging_Independent_Anonymity/Anonymity.thy

thys/Logging_Independent_Anonymity/Definitions.thy

thys/Logging_Independent_Anonymity/Possibility.thy

thys/Logging_Independent_Anonymity/ROOT

thys/Logging_Independent_Anonymity/document/root.bib

thys/Logging_Independent_Anonymity/document/root.tex

thys/ROOTS

thys/Schutz_Spacetime/Minkowski.thy

thys/Schutz_Spacetime/ROOT

thys/Schutz_Spacetime/TemporalOrderOnPath.thy

thys/Schutz_Spacetime/TernaryOrdering.thy

thys/Schutz_Spacetime/Util.thy

thys/Schutz_Spacetime/document/root.bib

thys/Schutz_Spacetime/document/root.tex

thys/Types_To_Sets_Extension/ETTS/ETTS.thy

thys/Types_To_Sets_Extension/ETTS/ETTS_Active.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Algorithm.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Auxiliary.thy

thys/Types_To_Sets_Extension/ETTS/ETTS_Context.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Lemma.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Lemmas.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_RI.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Substitution.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tactics.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/ETTS_Tools.thy

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/ETTS_Writer.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_HOLogic.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Library.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Logic.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Simplifier.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Tactical.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Term.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Transfer.ML

thys/Types_To_Sets_Extension/ETTS/ETTS_Utilities.ML

thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_CR.thy

thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Examples.thy

thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Introduction.thy

thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Syntax.thy

thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Theory.thy

thys/Types_To_Sets_Extension/ETTS/Manual/Manual_Prerequisites.thy

thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_AMEND_CTXT_DATA.ML

thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML

thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_REGISTER_SBTS.ML

thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy

thys/Types_To_Sets_Extension/Examples/Introduction.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Algebra/SML_Groups.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Algebra/SML_Monoids.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Algebra/SML_Rings.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Algebra/SML_Semigroups.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Algebra/SML_Semirings.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Foundations/Lifting_Set_Ext.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Foundations/Product_Type_Ext.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Foundations/SML_Relations.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Foundations/Set_Ext.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Foundations/Transfer_Ext.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Lattices.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Linorders.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Semilattices.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/SML_Conclusions.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/SML_Introduction.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Ordered_Topological_Spaces.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Product_Topology.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Topological_Space.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Topological_Space_Countability.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Algebra/Set_Semigroups.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Algebra/Type_Semigroups.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/FNDS_Conclusions.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/FNDS_Introduction.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Foundations/FNDS_Auxiliary.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Foundations/FNDS_Definite_Description.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Foundations/FNDS_Lifting_Set_Ext.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Foundations/FNDS_Set_Ext.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Orders/Set_Simple_Orders.thy

thys/Types_To_Sets_Extension/Examples/TTS_Foundations/Orders/Type_Simple_Orders.thy

thys/Types_To_Sets_Extension/Examples/Vector_Spaces/VS_Conclusions.thy

thys/Types_To_Sets_Extension/Examples/Vector_Spaces/VS_Groups.thy

thys/Types_To_Sets_Extension/Examples/Vector_Spaces/VS_Modules.thy

thys/Types_To_Sets_Extension/Examples/Vector_Spaces/VS_Prerequisites.thy

thys/Types_To_Sets_Extension/Examples/Vector_Spaces/VS_Vector_Spaces.thy

thys/Types_To_Sets_Extension/LICENSE

thys/Types_To_Sets_Extension/ROOT

thys/Types_To_Sets_Extension/document/extra.sty

thys/Types_To_Sets_Extension/document/iman.sty

thys/Types_To_Sets_Extension/document/isar.sty

thys/Types_To_Sets_Extension/document/root.bib

thys/Types_To_Sets_Extension/document/root.tex

thys/Types_To_Sets_Extension/document/style.sty

web/entries/Abstract-Rewriting.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/CZH_Elementary_Categories.html

web/entries/CZH_Foundations.html

web/entries/CZH_Universal_Constructions.html

web/entries/Conditional_Simplification.html

web/entries/Conditional_Transfer_Rule.html

web/entries/Containers.html

web/entries/Cubic_Quartic_Equations.html

web/entries/Dominance_CHK.html

web/entries/Efficient-Mergesort.html

web/entries/Gauss_Jordan.html

web/entries/Hermite_Lindemann.html

web/entries/Intro_Dest_Elim.html

web/entries/Logging_Independent_Anonymity.html

web/entries/Matrix.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Schutz_Spacetime.html

web/entries/Show.html

web/entries/Subresultants.html

web/entries/Types_To_Sets_Extension.html

web/entries/VectorSpace.html

web/entries/ZFC_in_HOL.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html