Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merge from afp 2020
  2. metadata and website for EFSMs
  3. changed short name of upcoming new entry as discussed with authors
  4. Fixed broken links (missing quote)
  5. sitegen for Robinson_Arithmetic
  6. new entry Robinson_Arithmetic
  7. missed for some reason
  8. Goedel_HFSet_Semanticless sitegen
  9. sitegen for Goedel_HFSet_Semantic
  10. new entry Goedel_HFSet_Semantic
  11. sitegen Goedel_Incompleteness
  12. new entry Goedel_Incompleteness
  13. sitegen for Syntax_Independent_Logic
  14. new entry Syntax_Independent_Logic
  15. new entry: Inference of Extended Finite State Machines
  16. new entry: Extended Finite State Machines
Changeset 11299:5172f1f451e6 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge from afp 2020
Changeset 11298:16b4ee88928e by rene thiemann _rene.thiemann@uibk.ac.at_:
metadata and website for EFSMs
The file was addedweb/entries/Extended_Finite_State_Machine_Inference.html
The file was addedweb/entries/Extended_Finite_State_Machines.html
The file was modified metadata/metadata
The file was modified web/entries/Automated_Stateful_Protocol_Verification.html
The file was modified web/entries/Core_DOM.html
The file was modified web/entries/Featherweight_OCL.html
The file was modified web/entries/FinFun.html
The file was modified web/entries/Stateful_Protocol_Composition_and_Typing.html
The file was modified web/entries/UPF.html
The file was modified web/entries/UPF_Firewall.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11297:83c401b5d938 by rene thiemann _rene.thiemann@uibk.ac.at_:
changed short name of upcoming new entry as discussed with authors
The file was addedthys/Extended_Finite_State_Machine_Inference/Code_Generation.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/EFSM_Dot.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/Inference.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/ROOT
The file was addedthys/Extended_Finite_State_Machine_Inference/SelectionStrategies.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/Subsumption.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_FSet.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_List.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/document/root.bib
The file was addedthys/Extended_Finite_State_Machine_Inference/document/root.tex
The file was addedthys/Extended_Finite_State_Machine_Inference/efsm2sal.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Distinguishing_Guards.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Group_By.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Increment_Reset.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/PTA_Generalisation.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Same_Register.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse_Subsumption.thy
The file was addedthys/Extended_Finite_State_Machine_Inference/heuristics/Weak_Subsumption.thy
The file was modified thys/ROOTS
The file was removedthys/EFSM_Inference/Code_Generation.thy
The file was removedthys/EFSM_Inference/EFSM_Dot.thy
The file was removedthys/EFSM_Inference/Inference.thy
The file was removedthys/EFSM_Inference/ROOT
The file was removedthys/EFSM_Inference/SelectionStrategies.thy
The file was removedthys/EFSM_Inference/Subsumption.thy
The file was removedthys/EFSM_Inference/code-targets/Code_Target_FSet.thy
The file was removedthys/EFSM_Inference/code-targets/Code_Target_List.thy
The file was removedthys/EFSM_Inference/code-targets/Code_Target_Set.thy
The file was removedthys/EFSM_Inference/document/root.bib
The file was removedthys/EFSM_Inference/document/root.tex
The file was removedthys/EFSM_Inference/efsm2sal.thy
The file was removedthys/EFSM_Inference/examples/Drinks_Subsumption.thy
The file was removedthys/EFSM_Inference/heuristics/Distinguishing_Guards.thy
The file was removedthys/EFSM_Inference/heuristics/Group_By.thy
The file was removedthys/EFSM_Inference/heuristics/Increment_Reset.thy
The file was removedthys/EFSM_Inference/heuristics/Least_Upper_Bound.thy
The file was removedthys/EFSM_Inference/heuristics/PTA_Generalisation.thy
The file was removedthys/EFSM_Inference/heuristics/Same_Register.thy
The file was removedthys/EFSM_Inference/heuristics/Store_Reuse.thy
The file was removedthys/EFSM_Inference/heuristics/Store_Reuse_Subsumption.thy
The file was removedthys/EFSM_Inference/heuristics/Weak_Subsumption.thy
Changeset 11296:7d13e8f13c83 by paulson _lp15@cam.ac.uk_:
Fixed broken links (missing quote)
The file was modified metadata/metadata
The file was modified web/entries/Goedel_HFSet_Semantic.html
The file was modified web/entries/Goedel_HFSet_Semanticless.html
The file was modified web/entries/Goedel_Incompleteness.html
The file was modified web/rss.xml
Changeset 11295:cd3f53ef34cf by paulson _lp15@cam.ac.uk_:
sitegen for Robinson_Arithmetic
The file was addedweb/entries/Robinson_Arithmetic.html
The file was modified metadata/metadata
The file was modified web/entries/Nominal2.html
The file was modified web/entries/Syntax_Independent_Logic.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11294:8907c16673c2 by paulson _lp15@cam.ac.uk_:
new entry Robinson_Arithmetic
The file was addedthys/Robinson_Arithmetic/Instance.thy
The file was addedthys/Robinson_Arithmetic/ROOT
The file was addedthys/Robinson_Arithmetic/Robinson_Arithmetic.thy
The file was addedthys/Robinson_Arithmetic/document/root.tex
The file was modified thys/ROOTS
Changeset 11293:0c168d703584 by paulson _lp15@cam.ac.uk_:
missed for some reason
The file was modified web/statistics.html
Changeset 11292:9db0d57a3eea by paulson _lp15@cam.ac.uk_:
Goedel_HFSet_Semanticless sitegen
The file was addedthys/Goedel_HFSet_Semanticless/Coding.thy
The file was addedthys/Goedel_HFSet_Semanticless/Coding_Predicates.thy
The file was addedthys/Goedel_HFSet_Semanticless/Functions.thy
The file was addedthys/Goedel_HFSet_Semanticless/Goedel_I.thy
The file was addedthys/Goedel_HFSet_Semanticless/II_Prelims.thy
The file was addedthys/Goedel_HFSet_Semanticless/Instance.thy
The file was addedthys/Goedel_HFSet_Semanticless/Pf_Predicates.thy
The file was addedthys/Goedel_HFSet_Semanticless/Predicates.thy
The file was addedthys/Goedel_HFSet_Semanticless/Pseudo_Coding.thy
The file was addedthys/Goedel_HFSet_Semanticless/Quote.thy
The file was addedthys/Goedel_HFSet_Semanticless/ROOT
The file was addedthys/Goedel_HFSet_Semanticless/Sigma.thy
The file was addedthys/Goedel_HFSet_Semanticless/SyntaxN.thy
The file was addedthys/Goedel_HFSet_Semanticless/document/root.tex
The file was addedweb/entries/Goedel_HFSet_Semanticless.html
The file was modified metadata/metadata
The file was modified thys/ROOTS
The file was modified web/entries/Goedel_Incompleteness.html
The file was modified web/entries/HereditarilyFinite.html
The file was modified web/entries/Nominal2.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/topics.html
Changeset 11291:049697b05aae by paulson _lp15@cam.ac.uk_:
sitegen for Goedel_HFSet_Semantic
The file was addedweb/entries/Goedel_HFSet_Semantic.html
The file was modified metadata/metadata
The file was modified web/entries/Goedel_Incompleteness.html
The file was modified web/entries/Incompleteness.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11290:74138bb55eee by paulson _lp15@cam.ac.uk_:
new entry Goedel_HFSet_Semantic
The file was addedthys/Goedel_HFSet_Semantic/Instance.thy
The file was addedthys/Goedel_HFSet_Semantic/ROOT
The file was addedthys/Goedel_HFSet_Semantic/document/root.tex
The file was modified thys/ROOTS
Changeset 11289:c75a30c27269 by paulson _lp15@cam.ac.uk_:
sitegen Goedel_Incompleteness
The file was addedweb/entries/Goedel_Incompleteness.html
The file was modified metadata/metadata
The file was modified web/entries/Syntax_Independent_Logic.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11288:2bddeb8064b6 by paulson _lp15@cam.ac.uk_:
new entry Goedel_Incompleteness
The file was addedthys/Goedel_Incompleteness/Abstract_Encoding.thy
The file was addedthys/Goedel_Incompleteness/Abstract_First_Goedel.thy
The file was addedthys/Goedel_Incompleteness/Abstract_First_Goedel_Rosser.thy
The file was addedthys/Goedel_Incompleteness/Abstract_Jeroslow_Encoding.thy
The file was addedthys/Goedel_Incompleteness/Abstract_Representability.thy
The file was addedthys/Goedel_Incompleteness/Abstract_Second_Goedel.thy
The file was addedthys/Goedel_Incompleteness/All_Abstract.thy
The file was addedthys/Goedel_Incompleteness/Deduction2.thy
The file was addedthys/Goedel_Incompleteness/Derivability_Conditions.thy
The file was addedthys/Goedel_Incompleteness/Diagonalization.thy
The file was addedthys/Goedel_Incompleteness/Goedel_Formula.thy
The file was addedthys/Goedel_Incompleteness/Jeroslow_Original.thy
The file was addedthys/Goedel_Incompleteness/Jeroslow_Simplified.thy
The file was addedthys/Goedel_Incompleteness/Loeb.thy
The file was addedthys/Goedel_Incompleteness/Loeb_Formula.thy
The file was addedthys/Goedel_Incompleteness/ROOT
The file was addedthys/Goedel_Incompleteness/Rosser_Formula.thy
The file was addedthys/Goedel_Incompleteness/Standard_Model_More.thy
The file was addedthys/Goedel_Incompleteness/Tarski.thy
The file was addedthys/Goedel_Incompleteness/document/root.bib
The file was addedthys/Goedel_Incompleteness/document/root.tex
The file was modified thys/ROOTS
Changeset 11287:1e4a662fb9f9 by paulson _lp15@cam.ac.uk_:
sitegen for Syntax_Independent_Logic
The file was addedweb/entries/Syntax_Independent_Logic.html
The file was modified metadata/metadata
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11286:1c25a24f6628 by paulson _lp15@cam.ac.uk_:
new entry Syntax_Independent_Logic
The file was addedthys/Syntax_Independent_Logic/Deduction.thy
The file was addedthys/Syntax_Independent_Logic/Deduction_Q.thy
The file was addedthys/Syntax_Independent_Logic/Natural_Deduction.thy
The file was addedthys/Syntax_Independent_Logic/Prelim.thy
The file was addedthys/Syntax_Independent_Logic/Pseudo_Term.thy
The file was addedthys/Syntax_Independent_Logic/ROOT
The file was addedthys/Syntax_Independent_Logic/Standard_Model.thy
The file was addedthys/Syntax_Independent_Logic/Syntax.thy
The file was addedthys/Syntax_Independent_Logic/Syntax_Arith.thy
The file was addedthys/Syntax_Independent_Logic/document/root.bib
The file was addedthys/Syntax_Independent_Logic/document/root.tex
The file was modified thys/ROOTS
Changeset 11285:32a273a24cd4 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Inference of Extended Finite State Machines
The file was addedthys/EFSM_Inference/Code_Generation.thy
The file was addedthys/EFSM_Inference/EFSM_Dot.thy
The file was addedthys/EFSM_Inference/Inference.thy
The file was addedthys/EFSM_Inference/ROOT
The file was addedthys/EFSM_Inference/SelectionStrategies.thy
The file was addedthys/EFSM_Inference/Subsumption.thy
The file was addedthys/EFSM_Inference/code-targets/Code_Target_FSet.thy
The file was addedthys/EFSM_Inference/code-targets/Code_Target_List.thy
The file was addedthys/EFSM_Inference/code-targets/Code_Target_Set.thy
The file was addedthys/EFSM_Inference/document/root.bib
The file was addedthys/EFSM_Inference/document/root.tex
The file was addedthys/EFSM_Inference/efsm2sal.thy
The file was addedthys/EFSM_Inference/examples/Drinks_Subsumption.thy
The file was addedthys/EFSM_Inference/heuristics/Distinguishing_Guards.thy
The file was addedthys/EFSM_Inference/heuristics/Group_By.thy
The file was addedthys/EFSM_Inference/heuristics/Increment_Reset.thy
The file was addedthys/EFSM_Inference/heuristics/Least_Upper_Bound.thy
The file was addedthys/EFSM_Inference/heuristics/PTA_Generalisation.thy
The file was addedthys/EFSM_Inference/heuristics/Same_Register.thy
The file was addedthys/EFSM_Inference/heuristics/Store_Reuse.thy
The file was addedthys/EFSM_Inference/heuristics/Store_Reuse_Subsumption.thy
The file was addedthys/EFSM_Inference/heuristics/Weak_Subsumption.thy
The file was modified thys/ROOTS
Changeset 11284:662f9db2d729 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Extended Finite State Machines
The file was addedthys/Extended_Finite_State_Machines/AExp.thy
The file was addedthys/Extended_Finite_State_Machines/AExp_Lexorder.thy
The file was addedthys/Extended_Finite_State_Machines/EFSM.thy
The file was addedthys/Extended_Finite_State_Machines/EFSM_LTL.thy
The file was addedthys/Extended_Finite_State_Machines/FSet_Utils.thy
The file was addedthys/Extended_Finite_State_Machines/GExp.thy
The file was addedthys/Extended_Finite_State_Machines/GExp_Lexorder.thy
The file was addedthys/Extended_Finite_State_Machines/README.md
The file was addedthys/Extended_Finite_State_Machines/ROOT
The file was addedthys/Extended_Finite_State_Machines/Transition.thy
The file was addedthys/Extended_Finite_State_Machines/Transition_Lexorder.thy
The file was addedthys/Extended_Finite_State_Machines/Trilean.thy
The file was addedthys/Extended_Finite_State_Machines/VName.thy
The file was addedthys/Extended_Finite_State_Machines/Value.thy
The file was addedthys/Extended_Finite_State_Machines/Value_Lexorder.thy
The file was addedthys/Extended_Finite_State_Machines/document/root.bib
The file was addedthys/Extended_Finite_State_Machines/document/root.tex
The file was addedthys/Extended_Finite_State_Machines/examples/Drinks_Machine.thy
The file was addedthys/Extended_Finite_State_Machines/examples/Drinks_Machine_2.thy
The file was addedthys/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy
The file was modified thys/ROOTS