Theory Check_Autogenerated_Files

(*
 * This is an autogenerated file. Do not edit.
 * It was created using instantiate_laws.py.
 * It checks whether the other autogenerated files are up-to-date.
 *)

theory Check_Autogenerated_Files
  (* These imports are not actually needed, but in jEdit, they will conveniently trigger a re-execution of the checking code below upon changes. *)
  imports Laws_Classical Laws_Quantum Laws_Complement_Quantum
begin

ML ‹
let
  fun check kind file expected = let
    val content = File.read (Path.append (Resources.master_directory \<^theory>) (Path.basic file))
    val hash = SHA1.digest content |> SHA1.rep
    in
      if hash = expected then () else
      error (kind ^ " file " ^ file ^ " has changed.\nPlease run \"python3 instantiate_laws.py\" to recreated autogenerated files.\nExpected SHA1 hash " ^ expected ^ ", got " ^ hash)
    end
in
  check "Source" "Axioms_Classical.thy" "f4a0dac97bed23ec5b7c4cbf779f8eb2a12aa488";
  check "Source" "Axioms_Quantum.thy" "b1ac4a827c2b943202c03611176d3c723119d8e1";
  check "Source" "Laws.thy" "69af9fbe716d0f2a8a3d076e76cfac467d3b85e7";
  check "Source" "Laws_Complement.thy" "6065101853fa432ca4bd6fd3113315e856e21ecb";
  check "Generated" "Laws_Classical.thy" "5d72e496fdbf182770dd6db9b8f36d9eead8a966";
  check "Generated" "Laws_Complement_Quantum.thy" "c58ba1680287643d1c3f9b2b97d9784db8e1dd84";
  check "Generated" "Laws_Quantum.thy" "cbc500287329e0d0a5156881638e95bbc8e26306"
end
›

end