Diffusion afp-devel 4dcc15eef93e

merged from afp-2019
4dcc15eef93e
Actions

Tags

None

Subscribers

None

Description

merged from afp-2019

Details

Provenance

Lars Hupel <lars.hupel@mytum.de>

Authored on

Parents

rAFPff1095d29305: CakeML_Codegen website
rAFP0c3edf9248d5: add lemmas

Branches

Unknown

Tags

Unknown

Event Timeline

Merged Changes

0c3edf9248d5 add lemmas
Author
immler
Browse Repository
No Builds
No Audits
e90416b32a35 adjusted Prim_Dijkstra_Simple from 2019 to devel (: -> \<in>)
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
a8d1e146f641 merge from AFP 2019, broken: Priority_Search_Trees
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
676a75e041d9 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
8a032c8c5b06 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
683827a3f2a2 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
26167902b4d2 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
581aa08c667e abstracted from deterministic automata
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
86f544c41cb4 removed UNION
Author
nipkow
Browse Repository
No Builds
No Audits
d697df9a952b tuned
Author
nipkow
Browse Repository
No Builds
No Audits
3261ff4818d4 merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
ec3ff55171a9 tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
967caff984be a few corollaries
Author
traytel
Browse Repository
No Builds
No Audits
023d4c3c8ef8 typo
Author
Christian Sternagel
Browse Repository
No Builds
No Audits
1099e41870d8 even more appropriate fact name
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d91cf5dccf6a merged
Author
traytel
Browse Repository
No Builds
No Audits
76da667dfde4 tuned definition of value as suggested by an ITP reviewer
Author
traytel
Browse Repository
No Builds
No Audits
1c7ecec6a187 simplified proof
Author
nipkow
Browse Repository
No Builds
No Audits
c293c479d6b6 repaired proofs
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a9d827f1c5b1 moved some theorems into HOL main corpus
Author
florian.haftmann
Browse Repository
No Builds
No Audits
65974f61a998 official fact collection sign_simps
Author
florian.haftmann
Browse Repository
No Builds
No Audits
415b7b57be74 dropped unused session references
Author
florian.haftmann
Browse Repository
No Builds
No Audits
0546343b94d3 clear separation of types for bits (False / True) and Z2 (0 / 1)
Author
florian.haftmann
Browse Repository
No Builds
No Audits
ee7d766eb01a dropped weaker legacy alias;
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f6b91be1ab2d dropped former legacy input abbreviations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cf0914a2304e fix for previous commit
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
6197fe173c6f refactoring
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
ad3aff5eb868 minor adjustments to automata library
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
60862c9ef07b refactored degeneralization
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
dc3e35215567 updated basic theories
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
22263520f4c8 updated with guillemot syntax
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e6d3d109c89a updated to devel
Author
nipkow
Browse Repository
No Builds
No Audits
a5f6453144c6 fixed latex errors using babel
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
fb851cb1ca27 replaced ceiling brackets by guillemots
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
79d06abed2e0 consistency is provable
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
5c9417f37470 merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
a8e34b81e70f tuned timeout;
Author
makarius
Browse Repository
No Builds
No Audits
7149dd204040 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
87cfcf4d1dec update cartouches
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
ca143f3dbb79 LambdaAuth: remove lemmas moved to distribution
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
cd86f83a05bb merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
72f2f7d150d6 re-instate devel changeset 6edffc003761
Author
kleing
Browse Repository
No Builds
No Audits
753dc504efaf reset version to devel after release fork
Author
kleing
Browse Repository
No Builds
No Audits
a0d561998f20 closed branch
Author
kleing
Browse Repository
No Builds
No Audits
8e995d947fb0 closed pull-request branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
249c2b58d173 closed merged branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
ad14484777fc merged
Author
gerwin.klein@nicta.com.au
Browse Repository
No Builds
No Audits
e3e858bfc9eb merged
Author
kleing
Browse Repository
No Builds
No Audits
4bea345493dd Closed branch ltl
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits
53421953ad96 WIP/LTL Entry
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (88)

Path

Size

metadata/

CakeML_Backend.thy

CakeML_Byte.thy

CakeML_Correctness.thy

CakeML_Setup.thy

Composition.thy

CupCake_Env.thy

CupCake_Semantics.thy

Doc_Backend.thy

Doc_Compiler.thy

Doc_CupCake.thy

Doc_Preproc.thy

Doc_Rewriting.thy

Eval_Instances.thy

eval_instances.ML

Big_Step_Sterm.thy

Big_Step_Value.thy

Big_Step_Value_ML.thy

Rewriting_Nterm.thy

Rewriting_Pterm.thy

Rewriting_Pterm_Elim.thy

Rewriting_Sterm.thy

Rewriting_Term.thy

Constructors.thy

General_Rewriting.thy

HOL_Datatype.thy

Strong_Term.thy

Term_as_Value.thy

Terms_Extras.thy

hol_datatype.ML

Test_Composition.thy

Test_Datatypes.thy

Test_Embed_Data.thy

Test_Embed_Data2.thy

Test_Embed_Simple.thy

Test_Embed_Tree.thy

CakeML_Utils.thy

Compiler_Utils.thy

dynamic_unfold.ML

pattern_compatibility.ML

CakeML_Codegen.html

Constructor_Funs.html

Dict_Construction.html

Higher_Order_Terms.html

Native_Word.html

Pairing_Heap.html

Root_Balanced_Tree.html

statistics.html

rAFP4dcc15eef93e

metadata/metadata

Loading...

thys/CakeML_Codegen/Backend/CakeML_Backend.thy

Loading...

thys/CakeML_Codegen/Backend/CakeML_Byte.thy

Loading...

thys/CakeML_Codegen/Backend/CakeML_Correctness.thy

Loading...

thys/CakeML_Codegen/Backend/CakeML_Setup.thy

Loading...

thys/CakeML_Codegen/Compiler/Compiler.thy

Loading...

thys/CakeML_Codegen/Compiler/Composition.thy

Loading...

thys/CakeML_Codegen/CupCakeML/CupCake_Env.thy

Loading...

thys/CakeML_Codegen/CupCakeML/CupCake_Semantics.thy

Loading...

thys/CakeML_Codegen/Doc/Doc_Backend.thy

Loading...

thys/CakeML_Codegen/Doc/Doc_Compiler.thy

Loading...

thys/CakeML_Codegen/Doc/Doc_CupCake.thy

Loading...

thys/CakeML_Codegen/Doc/Doc_Preproc.thy

Loading...

thys/CakeML_Codegen/Doc/Doc_Rewriting.thy

Loading...

thys/CakeML_Codegen/Doc/Doc_Terms.thy

Loading...

thys/CakeML_Codegen/Preproc/Embed.thy

Loading...

thys/CakeML_Codegen/Preproc/Eval_Class.thy

Loading...

thys/CakeML_Codegen/Preproc/Eval_Instances.thy

Loading...

thys/CakeML_Codegen/Preproc/embed.ML

Loading...

thys/CakeML_Codegen/Preproc/eval_instances.ML

Loading...

thys/CakeML_Codegen/Preproc/tactics.ML

Loading...

thys/CakeML_Codegen/ROOT

Loading...

thys/CakeML_Codegen/Rewriting/Big_Step_Sterm.thy

Loading...

thys/CakeML_Codegen/Rewriting/Big_Step_Value.thy

Loading...

thys/CakeML_Codegen/Rewriting/Big_Step_Value_ML.thy

Loading...

thys/CakeML_Codegen/Rewriting/Rewriting_Nterm.thy

Loading...

thys/CakeML_Codegen/Rewriting/Rewriting_Pterm.thy

Loading...

thys/CakeML_Codegen/Rewriting/Rewriting_Pterm_Elim.thy

Loading...

thys/CakeML_Codegen/Rewriting/Rewriting_Sterm.thy

Loading...

thys/CakeML_Codegen/Rewriting/Rewriting_Term.thy

Loading...

thys/CakeML_Codegen/Terms/Constructors.thy

Loading...

thys/CakeML_Codegen/Terms/Consts.thy

Loading...

thys/CakeML_Codegen/Terms/General_Rewriting.thy

Loading...

thys/CakeML_Codegen/Terms/HOL_Datatype.thy

Loading...

thys/CakeML_Codegen/Terms/Pterm.thy

Loading...

thys/CakeML_Codegen/Terms/Sterm.thy

Loading...

thys/CakeML_Codegen/Terms/Strong_Term.thy

Loading...

thys/CakeML_Codegen/Terms/Term_as_Value.thy

Loading...

thys/CakeML_Codegen/Terms/Terms_Extras.thy

Loading...

thys/CakeML_Codegen/Terms/Value.thy

Loading...

thys/CakeML_Codegen/Terms/hol_datatype.ML

Loading...

thys/CakeML_Codegen/Terms/hol_term.ML

Loading...

thys/CakeML_Codegen/Test/Test_Composition.thy

Loading...

thys/CakeML_Codegen/Test/Test_Datatypes.thy

Loading...

thys/CakeML_Codegen/Test/Test_Embed_Data.thy

Loading...

thys/CakeML_Codegen/Test/Test_Embed_Data2.thy

Loading...

thys/CakeML_Codegen/Test/Test_Embed_Simple.thy

Loading...

thys/CakeML_Codegen/Test/Test_Embed_Tree.thy

Loading...

thys/CakeML_Codegen/Test/Test_Print.thy

Loading...

thys/CakeML_Codegen/Utils/CakeML_Utils.thy

Loading...

thys/CakeML_Codegen/Utils/Code_Utils.thy

Loading...

thys/CakeML_Codegen/Utils/Compiler_Utils.thy

Loading...

thys/CakeML_Codegen/Utils/ML_Utils.thy

Loading...

thys/CakeML_Codegen/Utils/Test_Utils.thy

Loading...

thys/CakeML_Codegen/Utils/dynamic_unfold.ML

Loading...

thys/CakeML_Codegen/Utils/pattern_compatibility.ML

Loading...

thys/CakeML_Codegen/Utils/utils.ML

Loading...

thys/CakeML_Codegen/document/root.tex

Loading...

thys/ROOTS

Loading...

web/entries/CakeML.html

Loading...

web/entries/CakeML_Codegen.html

Loading...

web/entries/Constructor_Funs.html

Loading...

web/entries/Deriving.html

Loading...

web/entries/Dict_Construction.html

Loading...

web/entries/Higher_Order_Terms.html

Loading...

web/entries/Huffman.html

Loading...

web/entries/Native_Word.html

Loading...

web/entries/Pairing_Heap.html

Loading...

web/entries/Root_Balanced_Tree.html

Loading...

web/entries/Show.html

Loading...

web/index.html

Loading...

web/rss.xml

Loading...

web/statistics.html

Loading...

web/topics.html

Loading...