Skip to content
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. more flexible syntax for theory load commands via Isabelle/Scala;
  3. clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically; propagate blob src_path from Scala to ML; clarified signature;
  4. proper structural equality;
  5. more explicit types;
  6. unused (see 7634d33c1a79);
  7. clarified signature;
  8. clarified modules;
  9. clarified file names;
  10. tuned signature;
  11. refined syntax for bundle mixins for locale and class specifications
Changeset 72749:38d001186621 by wenzelm:
merged
Changeset 72748:04d5f6d769a7 by wenzelm:
more flexible syntax for theory load commands via Isabelle/Scala;
The file was addedsrc/HOL/SPARK/Tools/spark.scala
The file was addedsrc/HOL/SPARK/etc/settings
The file was modified NEWS
The file was modified src/HOL/SPARK/SPARK_Setup.thy
The file was modified src/Pure/Isar/keyword.scala
The file was modified src/Pure/Isar/outer_syntax.scala
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/command_span.scala
The file was modified src/Pure/Thy/thy_header.scala
The file was modified src/Pure/Tools/scala_project.scala
The file was modified src/Pure/build-jars
Changeset 72747:5f9d66155081 by wenzelm:
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;<br>propagate blob src_path from Scala to ML;<br>clarified signature;
The file was modified src/HOL/SMT_Examples/boogie.ML
The file was modified src/HOL/SPARK/Tools/spark_commands.ML
The file was modified src/Pure/Isar/keyword.ML
The file was modified src/Pure/ML/ml_file.ML
The file was modified src/Pure/PIDE/command.ML
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/document.ML
The file was modified src/Pure/PIDE/protocol.ML
The file was modified src/Pure/PIDE/protocol.scala
The file was modified src/Pure/PIDE/resources.ML
The file was modified src/Pure/Pure.thy
The file was modified src/Pure/Thy/thy_header.ML
The file was modified src/Pure/Thy/thy_header.scala
Changeset 72746:049a71febf05 by wenzelm:
proper structural equality;
The file was modified src/Pure/General/path.scala
Changeset 72745:5a6f7212fc4d by wenzelm:
more explicit types;
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/protocol.scala
Changeset 72744:0017eb17ac1c by wenzelm:
unused (see 7634d33c1a79);
The file was modified src/Pure/General/symbol.scala
The file was modified src/Pure/Isar/token.scala
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/command_span.scala
Changeset 72743:bc82fc605424 by wenzelm:
clarified signature;
The file was modified src/Pure/PIDE/command_span.scala
Changeset 72742:bda424c5819f by wenzelm:
clarified modules;
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/command_span.scala
The file was modified src/Pure/PIDE/resources.scala
Changeset 72741:b808eddc83cf by wenzelm:
clarified file names;
The file was modified src/HOL/SMT_Examples/Boogie.thy
Changeset 72740:082200ee003d by wenzelm:
tuned signature;
The file was modified src/Pure/Isar/keyword.scala
The file was modified src/Pure/Isar/outer_syntax.scala
The file was modified src/Pure/PIDE/resources.scala
Changeset 72739:e7c2848b78e8 by haftmann:
refined syntax for bundle mixins for locale and class specifications
The file was modified NEWS
The file was modified src/Doc/Isar_Ref/Spec.thy
The file was modified src/HOL/Product_Type.thy
The file was modified src/HOL/ex/Specifications_with_bundle_mixins.thy
The file was modified src/Pure/Isar/parse_spec.ML
The file was modified src/Pure/Pure.thy

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

Summary

  1. opening is now a keyword
  2. sorted out lemmas
  3. 2 new devel entries: DOM_Components and Shadow_DOM
  4. merge from afp-2020
  5. SC_DOM_Components website
  6. entry SC_DOM_Components
  7. website for Shadow_SC_DOM
  8. new entry Shadow_SC_DOM
  9. website for Core_SC_DOM
  10. The first of Achim D. Brucker's three entries
  11. fixed latex and .bib errors
  12. Verified_SAT_Based_AI_Planning website [NB corrected some \cite commands and deleted some excess files]
  13. Verified_SAT_Based_AI_Planning files
  14. Entry for AI_Planning_Languages_Semantics, including new topic "Computer science/Artificial intelligence" and URLs for the authors
  15. new entry AI_Planning_Languages_Semantics
  16. sitegen and metadata for Physical Quantities
  17. new Entry: Physical Quantities
  18. updated the email addresses of Popescu <https://www.andreipopescu.uk> and Traytel <https://traytel.bitbucket.io>
Changeset 11448:a13bec92d3d2 by haftmann:
opening is now a keyword
The file was modified thys/Sigma_Commit_Crypto/Pedersen.thy
The file was modified thys/Sigma_Commit_Crypto/Rivest.thy
The file was modified thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy
Changeset 11447:69f3a2dbc505 by haftmann:
sorted out lemmas
The file was modified thys/IP_Addresses/Lib_Word_toString.thy
The file was modified thys/IP_Addresses/NumberWang_IPv6.thy
The file was modified thys/Simple_Firewall/Service_Matrix.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/Enumeration_Word.thy
The file was modified thys/Word_Lib/Even_More_List.thy
The file was modified thys/Word_Lib/More_Misc.thy
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/Traditional_Infix_Syntax.thy
The file was modified thys/Word_Lib/Typedef_Morphisms.thy
The file was modified thys/Word_Lib/Word_16.thy
The file was modified thys/Word_Lib/Word_8.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lib_Sumo.thy
Changeset 11446:11e9abcf7366 by kleing:
2 new devel entries: DOM_Components and Shadow_DOM
The file was addedthys/DOM_Components/Core_DOM_Components.thy
The file was addedthys/DOM_Components/ROOT
The file was addedthys/DOM_Components/Shadow_DOM_Components.thy
The file was addedthys/DOM_Components/counterexample/fancy-tabs.html
The file was addedthys/DOM_Components/counterexample/fancy_tabs.thy
The file was addedthys/DOM_Components/document/fancytabs-normal.jpg
The file was addedthys/DOM_Components/document/root.bib
The file was addedthys/DOM_Components/document/root.tex
The file was addedthys/Shadow_DOM/ROOT
The file was addedthys/Shadow_DOM/Shadow_DOM.thy
The file was addedthys/Shadow_DOM/Shadow_DOM_Tests.thy
The file was addedthys/Shadow_DOM/classes/ShadowRootClass.thy
The file was addedthys/Shadow_DOM/document/root.bib
The file was addedthys/Shadow_DOM/document/root.tex
The file was addedthys/Shadow_DOM/monads/ShadowRootMonad.thy
The file was addedthys/Shadow_DOM/tests/Document-adoptNode.html
The file was addedthys/Shadow_DOM/tests/Document-getElementById.html
The file was addedthys/Shadow_DOM/tests/Node-insertBefore.html
The file was addedthys/Shadow_DOM/tests/Node-removeChild.html
The file was addedthys/Shadow_DOM/tests/Shadow_DOM_BaseTest.thy
The file was addedthys/Shadow_DOM/tests/Shadow_DOM_Document_adoptNode.thy
The file was addedthys/Shadow_DOM/tests/Shadow_DOM_Document_getElementById.thy
The file was addedthys/Shadow_DOM/tests/Shadow_DOM_Node_insertBefore.thy
The file was addedthys/Shadow_DOM/tests/Shadow_DOM_Node_removeChild.thy
The file was addedthys/Shadow_DOM/tests/my_get_owner_document.html
The file was addedthys/Shadow_DOM/tests/my_get_owner_document.thy
The file was addedthys/Shadow_DOM/tests/slots-fallback.html
The file was addedthys/Shadow_DOM/tests/slots.html
The file was addedthys/Shadow_DOM/tests/slots.thy
The file was addedthys/Shadow_DOM/tests/slots_fallback.thy
The file was addedweb/entries/DOM_Components.html
The file was addedweb/entries/Shadow_DOM.html
The file was modified metadata/metadata
The file was modified thys/ROOTS
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/Core_SC_DOM.html
The file was modified web/entries/Extended_Finite_State_Machine_Inference.html
The file was modified web/entries/Extended_Finite_State_Machines.html
The file was modified web/entries/Featherweight_OCL.html
The file was modified web/entries/SC_DOM_Components.html
The file was modified web/entries/Shadow_SC_DOM.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 11445:707413df05fd by kleing:
merge from afp-2020
Changeset 11444:cace3e947231 by paulson _lp15@cam.ac.uk_:
SC_DOM_Components website
The file was addedweb/entries/SC_DOM_Components.html
The file was modified metadata/metadata
The file was modified web/entries/Shadow_SC_DOM.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 11443:93ce0b890f00 by paulson _lp15@cam.ac.uk_:
entry SC_DOM_Components
The file was addedthys/SC_DOM_Components/Core_DOM_DOM_Components.thy
The file was addedthys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy
The file was addedthys/SC_DOM_Components/ROOT
The file was addedthys/SC_DOM_Components/Shadow_DOM_DOM_Components.thy
The file was addedthys/SC_DOM_Components/Shadow_DOM_SC_DOM_Components.thy
The file was addedthys/SC_DOM_Components/document/fancytabs-normal.jpg
The file was addedthys/SC_DOM_Components/document/root.bib
The file was addedthys/SC_DOM_Components/document/root.tex
The file was modified thys/ROOTS
Changeset 11442:60dca93e29de by paulson _lp15@cam.ac.uk_:
website for Shadow_SC_DOM
The file was addedweb/entries/Shadow_SC_DOM.html
The file was modified metadata/metadata
The file was modified web/entries/Core_SC_DOM.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 11441:97e390b29fa8 by paulson _lp15@cam.ac.uk_:
new entry Shadow_SC_DOM
The file was addedthys/Shadow_SC_DOM/ROOT
The file was addedthys/Shadow_SC_DOM/Shadow_DOM.thy
The file was addedthys/Shadow_SC_DOM/Shadow_DOM_Tests.thy
The file was addedthys/Shadow_SC_DOM/classes/ShadowRootClass.thy
The file was addedthys/Shadow_SC_DOM/document/root.bib
The file was addedthys/Shadow_SC_DOM/document/root.tex
The file was addedthys/Shadow_SC_DOM/monads/ShadowRootMonad.thy
The file was addedthys/Shadow_SC_DOM/tests/Document-adoptNode.html
The file was addedthys/Shadow_SC_DOM/tests/Document-getElementById.html
The file was addedthys/Shadow_SC_DOM/tests/Node-insertBefore.html
The file was addedthys/Shadow_SC_DOM/tests/Node-removeChild.html
The file was addedthys/Shadow_SC_DOM/tests/Shadow_DOM_BaseTest.thy
The file was addedthys/Shadow_SC_DOM/tests/Shadow_DOM_Document_adoptNode.thy
The file was addedthys/Shadow_SC_DOM/tests/Shadow_DOM_Document_getElementById.thy
The file was addedthys/Shadow_SC_DOM/tests/Shadow_DOM_Node_insertBefore.thy
The file was addedthys/Shadow_SC_DOM/tests/Shadow_DOM_Node_removeChild.thy
The file was addedthys/Shadow_SC_DOM/tests/my_get_owner_document.html
The file was addedthys/Shadow_SC_DOM/tests/my_get_owner_document.thy
The file was addedthys/Shadow_SC_DOM/tests/slots-fallback.html
The file was addedthys/Shadow_SC_DOM/tests/slots.html
The file was addedthys/Shadow_SC_DOM/tests/slots.thy
The file was addedthys/Shadow_SC_DOM/tests/slots_fallback.thy
The file was modified thys/ROOTS
Changeset 11440:78358736c8d0 by paulson _lp15@cam.ac.uk_:
website for Core_SC_DOM
The file was addedweb/entries/Core_SC_DOM.html
Changeset 11439:16e23db9b0d3 by paulson _lp15@cam.ac.uk_:
The first of Achim D. Brucker&#039;s three entries
The file was addedthys/Core_SC_DOM/CITATION
The file was addedthys/Core_SC_DOM/ROOT
The file was addedthys/Core_SC_DOM/common/Core_DOM.thy
The file was addedthys/Core_SC_DOM/common/Core_DOM_Basic_Datatypes.thy
The file was addedthys/Core_SC_DOM/common/Core_DOM_Functions.thy
The file was addedthys/Core_SC_DOM/common/Core_DOM_Tests.thy
The file was addedthys/Core_SC_DOM/common/classes/BaseClass.thy
The file was addedthys/Core_SC_DOM/common/classes/CharacterDataClass.thy
The file was addedthys/Core_SC_DOM/common/classes/DocumentClass.thy
The file was addedthys/Core_SC_DOM/common/classes/NodeClass.thy
The file was addedthys/Core_SC_DOM/common/classes/ObjectClass.thy
The file was addedthys/Core_SC_DOM/common/monads/BaseMonad.thy
The file was addedthys/Core_SC_DOM/common/monads/CharacterDataMonad.thy
The file was addedthys/Core_SC_DOM/common/monads/DocumentMonad.thy
The file was addedthys/Core_SC_DOM/common/monads/ElementMonad.thy
The file was addedthys/Core_SC_DOM/common/monads/NodeMonad.thy
The file was addedthys/Core_SC_DOM/common/monads/ObjectMonad.thy
The file was addedthys/Core_SC_DOM/common/pointers/CharacterDataPointer.thy
The file was addedthys/Core_SC_DOM/common/pointers/DocumentPointer.thy
The file was addedthys/Core_SC_DOM/common/pointers/ElementPointer.thy
The file was addedthys/Core_SC_DOM/common/pointers/NodePointer.thy
The file was addedthys/Core_SC_DOM/common/pointers/ObjectPointer.thy
The file was addedthys/Core_SC_DOM/common/pointers/Ref.thy
The file was addedthys/Core_SC_DOM/common/preliminaries/Heap_Error_Monad.thy
The file was addedthys/Core_SC_DOM/common/preliminaries/Hiding_Type_Variables.thy
The file was addedthys/Core_SC_DOM/common/preliminaries/Testing_Utils.thy
The file was addedthys/Core_SC_DOM/common/tests/Core_DOM_BaseTest.thy
The file was addedthys/Core_SC_DOM/common/tests/Document-adoptNode.html
The file was addedthys/Core_SC_DOM/common/tests/Document-getElementById.html
The file was addedthys/Core_SC_DOM/common/tests/Document_adoptNode.thy
The file was addedthys/Core_SC_DOM/common/tests/Document_getElementById.thy
The file was addedthys/Core_SC_DOM/common/tests/Node-insertBefore.html
The file was addedthys/Core_SC_DOM/common/tests/Node-removeChild.html
The file was addedthys/Core_SC_DOM/common/tests/Node_insertBefore.thy
The file was addedthys/Core_SC_DOM/common/tests/Node_removeChild.thy
The file was addedthys/Core_SC_DOM/document/root.bib
The file was addedthys/Core_SC_DOM/document/root.tex
The file was addedthys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy
The file was addedthys/Core_SC_DOM/safely_composable/classes/ElementClass.thy
The file was addedthys/Core_SC_DOM/safely_composable/pointers/ShadowRootPointer.thy
The file was modified metadata/metadata
The file was modified thys/ROOTS
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 11438:014d0d5b7c4c by paulson _lp15@cam.ac.uk_:
fixed latex and .bib errors
The file was modified thys/Verified_SAT_Based_AI_Planning/ROOT
The file was modified thys/Verified_SAT_Based_AI_Planning/SAT_Plan_Base.thy
The file was modified thys/Verified_SAT_Based_AI_Planning/document/root.bib
Changeset 11437:ffad5ea62de0 by paulson _lp15@cam.ac.uk_:
Verified_SAT_Based_AI_Planning website [NB corrected some \cite commands and deleted some excess files]
The file was addedweb/entries/Verified_SAT_Based_AI_Planning.html
The file was modified metadata/metadata
The file was modified web/entries/AI_Planning_Languages_Semantics.html
The file was modified web/entries/List-Index.html
The file was modified web/entries/Propositional_Proof_Systems.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 11436:0113b6493114 by paulson _lp15@cam.ac.uk_:
Verified_SAT_Based_AI_Planning files
The file was addedthys/Verified_SAT_Based_AI_Planning/AST_SAS_Plus_Equivalence.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/CNF_Semantics_Supplement.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/CNF_Supplement.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/List_Supplement.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/Map_Supplement.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/ROOT
The file was addedthys/Verified_SAT_Based_AI_Planning/SAS_Plus_Representation.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/SAS_Plus_STRIPS.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/SAS_Plus_Semantics.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/SAT_Plan_Base.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/SAT_Plan_Extensions.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/SAT_Solve_SAS_Plus.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/STRIPS_Representation.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/STRIPS_Semantics.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/Set2_Join_RBT.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/Solve_SASP.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/State_Variable_Representation.thy
The file was addedthys/Verified_SAT_Based_AI_Planning/code/build.sh
The file was addedthys/Verified_SAT_Based_AI_Planning/code/compute_plan.sh
The file was addedthys/Verified_SAT_Based_AI_Planning/code/decode_model.mlb
The file was addedthys/Verified_SAT_Based_AI_Planning/code/decode_model.sml
The file was addedthys/Verified_SAT_Based_AI_Planning/code/encode_problem.mlb
The file was addedthys/Verified_SAT_Based_AI_Planning/code/encode_problem.sml
The file was addedthys/Verified_SAT_Based_AI_Planning/code/generated/SASP_to_DIMACS.sml
The file was addedthys/Verified_SAT_Based_AI_Planning/code/generated/decode_DIMACS_model.sml
The file was addedthys/Verified_SAT_Based_AI_Planning/code/sas_plus.sml
The file was addedthys/Verified_SAT_Based_AI_Planning/document/root.bib
The file was addedthys/Verified_SAT_Based_AI_Planning/document/root.tex
The file was modified thys/ROOTS
Changeset 11435:67cb08d893b5 by paulson _lp15@cam.ac.uk_:
Entry for AI_Planning_Languages_Semantics, including new topic &quot;Computer science/Artificial intelligence&quot; and URLs for the authors
The file was addedweb/entries/AI_Planning_Languages_Semantics.html
The file was modified metadata/metadata
The file was modified metadata/topics
The file was modified web/entries/Certification_Monads.html
The file was modified web/entries/Containers.html
The file was modified web/entries/Propositional_Proof_Systems.html
The file was modified web/entries/Show.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 11434:93f41fb311c0 by paulson _lp15@cam.ac.uk_:
new entry AI_Planning_Languages_Semantics
The file was addedthys/AI_Planning_Languages_Semantics/Error_Monad_Add.thy
The file was addedthys/AI_Planning_Languages_Semantics/Lifschitz_Consistency.thy
The file was addedthys/AI_Planning_Languages_Semantics/Option_Monad_Add.thy
The file was addedthys/AI_Planning_Languages_Semantics/PDDL_STRIPS_Checker.thy
The file was addedthys/AI_Planning_Languages_Semantics/PDDL_STRIPS_Semantics.thy
The file was addedthys/AI_Planning_Languages_Semantics/ROOT
The file was addedthys/AI_Planning_Languages_Semantics/SASP_Checker.thy
The file was addedthys/AI_Planning_Languages_Semantics/SASP_Semantics.thy
The file was addedthys/AI_Planning_Languages_Semantics/code/Makefile
The file was addedthys/AI_Planning_Languages_Semantics/code/PDDL_Checker.mlb
The file was addedthys/AI_Planning_Languages_Semantics/code/PDDL_Checker.sml
The file was addedthys/AI_Planning_Languages_Semantics/code/PDDL_Checker_Fluents.mlb
The file was addedthys/AI_Planning_Languages_Semantics/code/SASP_Checker_Exported.sml
The file was addedthys/AI_Planning_Languages_Semantics/code/Unsynchronized.sml
The file was addedthys/AI_Planning_Languages_Semantics/document/root.bib
The file was addedthys/AI_Planning_Languages_Semantics/document/root.tex
The file was modified thys/ROOTS
Changeset 11433:e02037dfc6c4 by rene thiemann _rene.thiemann@uibk.ac.at_:
sitegen and metadata for Physical Quantities
The file was addedweb/entries/Physical_Quantities.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 11432:2ad0e69218eb by rene thiemann _rene.thiemann@uibk.ac.at_:
new Entry: Physical Quantities
The file was addedthys/Physical_Quantities/BIS.thy
The file was addedthys/Physical_Quantities/CGS.thy
The file was addedthys/Physical_Quantities/Enum_extra.thy
The file was addedthys/Physical_Quantities/Groups_mult.thy
The file was addedthys/Physical_Quantities/ISQ.thy
The file was addedthys/Physical_Quantities/ISQ_Algebra.thy
The file was addedthys/Physical_Quantities/ISQ_Conversion.thy
The file was addedthys/Physical_Quantities/ISQ_Dimensions.thy
The file was addedthys/Physical_Quantities/ISQ_Proof.thy
The file was addedthys/Physical_Quantities/ISQ_Quantities.thy
The file was addedthys/Physical_Quantities/ISQ_Units.thy
The file was addedthys/Physical_Quantities/Power_int.thy
The file was addedthys/Physical_Quantities/ROOT
The file was addedthys/Physical_Quantities/SI.thy
The file was addedthys/Physical_Quantities/SI_Accepted.thy
The file was addedthys/Physical_Quantities/SI_Astronomical.thy
The file was addedthys/Physical_Quantities/SI_Constants.thy
The file was addedthys/Physical_Quantities/SI_Derived.thy
The file was addedthys/Physical_Quantities/SI_Imperial.thy
The file was addedthys/Physical_Quantities/SI_Prefix.thy
The file was addedthys/Physical_Quantities/SI_Pretty.thy
The file was addedthys/Physical_Quantities/SI_Units.thy
The file was addedthys/Physical_Quantities/document/adb-long.bib
The file was addedthys/Physical_Quantities/document/root.bib
The file was addedthys/Physical_Quantities/document/root.tex
The file was modified thys/ROOTS
Changeset 11431:9a5a901c932d by paulson _lp15@cam.ac.uk_:
updated the email addresses of Popescu &lt;https://www.andreipopescu.uk&gt; and Traytel &lt;https://traytel.bitbucket.io&gt;
The file was modified metadata/metadata
The file was modified web/entries/Abstract_Completeness.html
The file was modified web/entries/Abstract_Soundness.html
The file was modified web/entries/BNF_Operations.html
The file was modified web/entries/Binding_Syntax_Theory.html
The file was modified web/entries/Bounded_Deducibility_Security.html
The file was modified web/entries/Chandy_Lamport.html
The file was modified web/entries/Coinductive_Languages.html
The file was modified web/entries/Formula_Derivatives.html
The file was modified web/entries/Functional_Ordered_Resolution_Prover.html
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/entries/HyperCTL.html
The file was modified web/entries/LambdaAuth.html
The file was modified web/entries/MFODL_Monitor_Optimized.html
The file was modified web/entries/MFOTL_Monitor.html
The file was modified web/entries/MSO_Regex_Equivalence.html
The file was modified web/entries/Nested_Multisets_Ordinals.html
The file was modified web/entries/Ordered_Resolution_Prover.html
The file was modified web/entries/Ordinals_and_Cardinals.html
The file was modified web/entries/Possibilistic_Noninterference.html
The file was modified web/entries/Probabilistic_Noninterference.html
The file was modified web/entries/Probabilistic_System_Zoo.html
The file was modified web/entries/Regex_Equivalence.html
The file was modified web/entries/Robinson_Arithmetic.html
The file was modified web/entries/Sliding_Window_Algorithm.html
The file was modified web/entries/Sort_Encodings.html
The file was modified web/entries/Syntax_Independent_Logic.html
The file was modified web/index.html