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" "452d79ff2f63da91f5d609d6e3565806cc5cce33";
  check "Source" "Laws.thy" "553c7f293ae03bb547c92f7039ded572a0f2337a";
  check "Source" "Laws_Complement.thy" "70f024eda3537a80716edaa1d921a5c1caf921bc";
  check "Generated" "Laws_Classical.thy" "3511dbbce24e00661e2d00382e630b28bad30130";
  check "Generated" "Laws_Complement_Quantum.thy" "4f53b2cbf551073cdeab7aceaa2b67612e4644ec";
  check "Generated" "Laws_Quantum.thy" "fc0524a1da55603ec54267c7e0dc50f0e01f1c3c"
end
›

end