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" "37803f67bcda2df6bf7abe2417d3bf49e6317dcd";
  check "Source" "Laws_Complement.thy" "6065101853fa432ca4bd6fd3113315e856e21ecb";
  check "Generated" "Laws_Classical.thy" "051bc83ae9bd061fba08bfa29468a3421817068b";
  check "Generated" "Laws_Complement_Quantum.thy" "c58ba1680287643d1c3f9b2b97d9784db8e1dd84";
  check "Generated" "Laws_Quantum.thy" "36d05e686993e4f9b7c5bf57639d840b3e9b2e47"
end


end