Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. WebAssembly: disable failing OCaml check
  2. BNF_CC: update to latest Isabelle syntax
  3. WebAssembly: update to latest Isabelle syntax
  4. merged from afp-2017
  5. New entry WebAssembly
  6. missing chapter
  7. new entry: BNF_CC
  8. The actual new entry Fishburn_Impossibility
  9. New entry Fishburn_Impossibility
Changeset 9155:29b886b790d2 by lars hupel _lars.hupel@mytum.de_:
WebAssembly: disable failing OCaml check
The file was modified thys/WebAssembly/Wasm_Printing/Wasm_Interpreter_Printing_Pure.thy (diff)
The file was modified thys/WebAssembly/Wasm_Printing/Wasm_Printing.thy (diff)
Changeset 9154:b241c318c856 by lars hupel _lars.hupel@mytum.de_:
BNF_CC: update to latest Isabelle syntax
The file was modified thys/BNF_CC/Axiomatised_BNF_CC.thy (diff)
The file was modified thys/BNF_CC/Composition.thy (diff)
The file was modified thys/BNF_CC/Concrete_Examples.thy (diff)
The file was modified thys/BNF_CC/DDS.thy (diff)
The file was modified thys/BNF_CC/Fixpoints.thy (diff)
The file was modified thys/BNF_CC/Preliminaries.thy (diff)
The file was modified thys/BNF_CC/Subtypes.thy (diff)
Changeset 9153:7cfc1093b23e by lars hupel _lars.hupel@mytum.de_:
WebAssembly: update to latest Isabelle syntax
The file was modified thys/WebAssembly/Wasm.thy (diff)
The file was modified thys/WebAssembly/Wasm_Ast.thy (diff)
Changeset 9152:96fb7f608fea by lars hupel _lars.hupel@mytum.de_:
merged from afp-2017
Changeset 9151:cd252db19441 by nipkow:
New entry WebAssembly
The file was addedthys/WebAssembly/ROOT
The file was addedthys/WebAssembly/Wasm.thy
The file was addedthys/WebAssembly/Wasm_Ast.thy
The file was addedthys/WebAssembly/Wasm_Axioms.thy
The file was addedthys/WebAssembly/Wasm_Base_Defs.thy
The file was addedthys/WebAssembly/Wasm_Checker.thy
The file was addedthys/WebAssembly/Wasm_Checker_Properties.thy
The file was addedthys/WebAssembly/Wasm_Checker_Types.thy
The file was addedthys/WebAssembly/Wasm_Interpreter.thy
The file was addedthys/WebAssembly/Wasm_Interpreter_Properties.thy
The file was addedthys/WebAssembly/Wasm_Printing/Wasm_Checker_Printing.thy
The file was addedthys/WebAssembly/Wasm_Printing/Wasm_Interpreter_Printing.thy
The file was addedthys/WebAssembly/Wasm_Printing/Wasm_Interpreter_Printing_Pure.thy
The file was addedthys/WebAssembly/Wasm_Printing/Wasm_Printing.thy
The file was addedthys/WebAssembly/Wasm_Printing/Wasm_Type_Abs_Printing.thy
The file was addedthys/WebAssembly/Wasm_Properties.thy
The file was addedthys/WebAssembly/Wasm_Properties_Aux.thy
The file was addedthys/WebAssembly/Wasm_Soundness.thy
The file was addedthys/WebAssembly/Wasm_Type_Abs.thy
The file was addedthys/WebAssembly/document/root.bib
The file was addedthys/WebAssembly/document/root.tex
The file was addedweb/entries/WebAssembly.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Native_Word.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 9150:c7cbe68ad140 by nipkow:
missing chapter
The file was modified thys/BNF_CC/ROOT (diff)
Changeset 9149:5ceb7a9317e0 by nipkow:
new entry: BNF_CC
The file was addedthys/BNF_CC/Axiomatised_BNF_CC.thy
The file was addedthys/BNF_CC/Composition.thy
The file was addedthys/BNF_CC/Concrete_Examples.thy
The file was addedthys/BNF_CC/DDS.thy
The file was addedthys/BNF_CC/Fixpoints.thy
The file was addedthys/BNF_CC/Operation_Examples.thy
The file was addedthys/BNF_CC/Preliminaries.thy
The file was addedthys/BNF_CC/Quotient_Preservation.thy
The file was addedthys/BNF_CC/ROOT
The file was addedthys/BNF_CC/Subtypes.thy
The file was addedthys/BNF_CC/document/root.bib
The file was addedthys/BNF_CC/document/root.tex
The file was addedweb/entries/BNF_CC.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Applicative_Lifting.html (diff)
The file was modified web/entries/Coinductive.html (diff)
The file was modified web/entries/Containers.html (diff)
The file was modified web/entries/CryptHOL.html (diff)
The file was modified web/entries/FinFun.html (diff)
The file was modified web/entries/Game_Based_Crypto.html (diff)
The file was modified web/entries/JinjaThreads.html (diff)
The file was modified web/entries/MFMC_Countable.html (diff)
The file was modified web/entries/Monad_Normalisation.html (diff)
The file was modified web/entries/Monomorphic_Monad.html (diff)
The file was modified web/entries/Native_Word.html (diff)
The file was modified web/entries/Probabilistic_System_Zoo.html (diff)
The file was modified web/entries/Probabilistic_While.html (diff)
The file was modified web/entries/Stern_Brocot.html (diff)
The file was modified web/entries/Stream_Fusion_Code.html (diff)
The file was modified web/entries/Trie.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 9148:43a8bb1dca1f by nipkow:
The actual new entry Fishburn_Impossibility
The file was addedthys/Fishburn_Impossibility/Fishburn_Impossibility.thy
The file was addedthys/Fishburn_Impossibility/ROOT
The file was addedthys/Fishburn_Impossibility/Social_Choice_Functions.thy
The file was addedthys/Fishburn_Impossibility/document/root.bib
The file was addedthys/Fishburn_Impossibility/document/root.tex
The file was addedweb/entries/Fishburn_Impossibility.html
Changeset 9147:2045f49fdd9d by nipkow:
New entry Fishburn_Impossibility
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Akra_Bazzi.html (diff)
The file was modified web/entries/Bernoulli.html (diff)
The file was modified web/entries/Bertrands_Postulate.html (diff)
The file was modified web/entries/Buffons_Needle.html (diff)
The file was modified web/entries/Catalan_Numbers.html (diff)
The file was modified web/entries/Comparison_Sort_Lower_Bound.html (diff)
The file was modified web/entries/Density_Compiler.html (diff)
The file was modified web/entries/Descartes_Sign_Rule.html (diff)
The file was modified web/entries/Dirichlet_Series.html (diff)
The file was modified web/entries/E_Transcendental.html (diff)
The file was modified web/entries/Error_Function.html (diff)
The file was modified web/entries/Euler_MacLaurin.html (diff)
The file was modified web/entries/Fisher_Yates.html (diff)
The file was modified web/entries/Landau_Symbols.html (diff)
The file was modified web/entries/Linear_Recurrences.html (diff)
The file was modified web/entries/Liouville_Numbers.html (diff)
The file was modified web/entries/Mason_Stothers.html (diff)
The file was modified web/entries/Median_Of_Medians_Selection.html (diff)
The file was modified web/entries/Minkowskis_Theorem.html (diff)
The file was modified web/entries/Monad_Normalisation.html (diff)
The file was modified web/entries/Prime_Harmonic_Series.html (diff)
The file was modified web/entries/Quick_Sort_Cost.html (diff)
The file was modified web/entries/Random_BSTs.html (diff)
The file was modified web/entries/Randomised_Social_Choice.html (diff)
The file was modified web/entries/SDS_Impossibility.html (diff)
The file was modified web/entries/Stirling_Formula.html (diff)
The file was modified web/entries/Sturm_Sequences.html (diff)
The file was modified web/entries/Treaps.html (diff)
The file was modified web/entries/Triangle.html (diff)
The file was modified web/entries/Zeta_Function.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)