Diffusion afp-devel d3f9882dd945

merged
d3f9882dd945
Actions

Description

merged

Details

Provenance

paulson

Authored on

Parents

rAFP757cd45633e5: New entry AOT
rAFP086e65efb46c: New entry: Propositional_Logic_Class

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rAFPd3f9882dd945: merged.Jan 12 2023, 1:24 PM

Merged Changes

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

086e65efb46c New entry: Propositional_Logic_Class
Author
nipkow
Browse Repository
No Builds
No Audits
db93f67adfd0 generalized theory name: euclidean division denotes one particular division…
Author
florian.haftmann
Browse Repository
No Builds
No Audits
75e99d0e6664 more efficient specification
Author
florian.haftmann
Browse Repository
No Builds
No Audits
95ab3b6c963f Removal of more unused material
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c8f289838f39 Small simplifications. Removed a needless assumption.
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
3080fbfdf9ff isabelle update -u cite;
Author
makarius
Browse Repository
No Builds
No Audits
1e054c418790 more accurate root.bib, based on original \bibitem entries in root.tex…
Author
makarius
Browse Repository
No Builds
No Audits
a2d9f49d2e53 Fixed the bib issues and supplied a root.bib based on the one in…
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
2996b211d242 merged
Author
paulson
Browse Repository
No Builds
No Audits
5f71be543faf Added the missing .bib file
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
735f4be0a671 proper bib context for formal citations, although there is no document;
Author
makarius
Browse Repository
No Builds
No Audits
65313718e1fe back to unchecked \cite: entry lacks .bib file;
Author
makarius
Browse Repository
No Builds
No Audits
a3ec1b73b356 back to unchecked \cite: entry lacks .bib file;
Author
makarius
Browse Repository
No Builds
No Audits
145b267c19cc back to unchecked \cite: there is entry lacks .bib file;
Author
makarius
Browse Repository
No Builds
No Audits
9ad9e3c39744 proper citation;
Author
makarius
Browse Repository
No Builds
No Audits
b41c90ddaf38 merged
Author
desharna
Browse Repository
No Builds
No Audits
e043b924a3e1 added lemmas image_grounding_of_cls_grounding_of_cls and…
Author
desharna
Browse Repository
No Builds
No Audits
158888c95cb5 merged
Author
makarius
Browse Repository
No Builds
No Audits
bd12d9b46e51 isabelle update -u cite;
Author
makarius
Browse Repository
No Builds
No Audits
9b889a22dc8c clse branch
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
69d56d231e8d merged
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
a581d4cc6671 consistent casing in \cite
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
493d027d541e ETTS: updated bibliography and citations
Author
user9716869 <user9716869@gmail.com>
Browse Repository
No Builds
No Audits
a5be6b3284e3 merged
Author
makarius
Browse Repository
No Builds
No Audits
b5cf1b3eb582 more correct and complete citations;
Author
makarius
Browse Repository
No Builds
No Audits
b1b1e175c5f8 unchecked \cite for unidentifiable citation;
Author
makarius
Browse Repository
No Builds
No Audits
d82316670919 proper @{cite} syntax;
Author
makarius
Browse Repository
No Builds
No Audits
ab90e6e586ca isabelle update -u cite;
Author
makarius
Browse Repository
No Builds
No Audits
1ce244e01035 Updating Risk Free Lending Entry
Author
Matthew Doty <matt@w-d.org>
Browse Repository
No Builds
No Audits
3090aa3b36a4 added bibliography to ROOT;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a3851542d034 CTR and ETTS: several amendments (fact names, printing, presentation)
Author
user9716869 <user9716869@gmail.com>
Browse Repository
No Builds
No Audits
af306ae40d20 Removed a reference to the (redundant) wf_restr
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
4b49cee6b5c7 added bibliographies to ROOTs;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f7dc857b7e3b Changes for generalised lemmas
Author
Katharina Kreuzer
Browse Repository
No Builds
No Audits
e39d82cd7a9d Changes for generalised lemmas
Author
Katharina Kreuzer
Browse Repository
No Builds
No Audits
edfb67bf875e Generalised Lemmas
Author
Katharina Kreuzer
Browse Repository
No Builds
No Audits
41a4bc0bcef1 merged
Author
desharna
Browse Repository
No Builds
No Audits
f63d39eac6e3 adapted to Isabelle/c9e091867206
Author
desharna
Browse Repository
No Builds
No Audits
8dc853888b8c tuned;
Author
makarius
Browse Repository
No Builds
No Audits
b4655cdb7be1 tuned signature, following Isabelle/947510ce4e36;
Author
makarius
Browse Repository
No Builds
No Audits
415f66ca9ad1 adapted to Isabelle/25900fbea7ad;
Author
makarius
Browse Repository
No Builds
No Audits
eba886159d27 adapted to Isabelle/b61ad889dffa
Author
desharna
Browse Repository
No Builds
No Audits
ff976ab985f2 removed Restricted_Predicates.transp_on following the introduction of…
Author
desharna
Browse Repository
No Builds
No Audits
7713c04dccf5 merged
Author
desharna
Browse Repository
No Builds
No Audits
13c86139b9cb adapted to Isabelle/d33fc5228aae
Author
desharna
Browse Repository
No Builds
No Audits
526b66ccd04f fixed proof following Isabelle/66cae055ac7b
Author
desharna
Browse Repository
No Builds
No Audits
f31fa8686572 merge
Author
blanchette
Browse Repository
No Builds
No Audits
98654eb7841b adapted to Isabelle/c48fe2be847f
Author
blanchette
Browse Repository
No Builds
No Audits
95bd9902bb57 enable -no-pie for CakeML
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
49df37cde100 fixed proofs and removed duplicates following Isabelle/e65a50f6c2de
Author
desharna
Browse Repository
No Builds
No Audits

Changes (22)

Path

Size

thys

AOT

AOT_Axioms.thy

AOT_BasicLogicalObjects.thy

AOT_Definitions.thy

AOT_ExtendedRelationComprehension.thy

AOT_NaturalNumbers.thy

AOT_PLM.thy

AOT_PossibleWorlds.thy

AOT_RestrictedVariables.thy

rAFPd3f9882dd945

View Options

thys/AOT/AOT_Axioms.thy

View Options

thys/AOT/AOT_BasicLogicalObjects.thy

View Options

thys/AOT/AOT_Definitions.thy

View Options

thys/AOT/AOT_ExtendedRelationComprehension.thy

View Options

thys/AOT/AOT_NaturalNumbers.thy

View Options

thys/AOT/AOT_PLM.thy

View Options

thys/AOT/AOT_PossibleWorlds.thy

View Options

thys/AOT/AOT_RestrictedVariables.thy

View Options

thys/AOT/AOT_commands.ML

View Options

thys/AOT/AOT_commands.thy

View Options

thys/AOT/AOT_keys.ML

View Options

thys/AOT/AOT_misc.thy

View Options

thys/AOT/AOT_model.thy

View Options

thys/AOT/AOT_semantics.thy

View Options

thys/AOT/AOT_syntax.ML

View Options

thys/AOT/AOT_syntax.thy

View Options

thys/AOT/ROOT

View Options

thys/AOT/document/root.tex

View Options

mergedd3f9882dd945Actions

Description

Details

Event Timeline

Merged Changes

Changes (22)

rAFPd3f9882dd945

thys/AOT/AOT_Axioms.thy

thys/AOT/AOT_BasicLogicalObjects.thy

thys/AOT/AOT_Definitions.thy

thys/AOT/AOT_ExtendedRelationComprehension.thy

thys/AOT/AOT_NaturalNumbers.thy

thys/AOT/AOT_PLM.thy

thys/AOT/AOT_PossibleWorlds.thy

thys/AOT/AOT_RestrictedVariables.thy

thys/AOT/AOT_commands.ML

thys/AOT/AOT_commands.thy

thys/AOT/AOT_keys.ML

thys/AOT/AOT_misc.thy

thys/AOT/AOT_model.thy

thys/AOT/AOT_semantics.thy

thys/AOT/AOT_syntax.ML

thys/AOT/AOT_syntax.thy

thys/AOT/ROOT

thys/AOT/document/root.tex

thys/ROOTS

merged
d3f9882dd945
Actions