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" "e3c6ca3fa815506631517ea5d682c23c08f4ed4f";
  check "Source" "Axioms_Quantum.thy" "eaa50706b1a7d09ca9ce4530c86f81e501937589";
  check "Source" "Laws.thy" "65ab3f7e71975cd14617f501b65a6acadceb1ef3";
  check "Source" "Laws_Complement.thy" "70ce14ff0247460eb56e09b8a5ed7b2715abebe0";
  check "Generated" "Laws_Classical.thy" "8a50d01926a3dabda71b8992451bf4acfb420654";
  check "Generated" "Laws_Complement_Quantum.thy" "fdc4022c54b9a5f2a95de15c6c391727e1b3bcc1";
  check "Generated" "Laws_Quantum.thy" "38a1ec5c464069098cb5855ace1d69fc49aea29b"
end
›

end