Theory PAC_Version

(*
  File:         PAC_Version.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Version
  imports Main
begin

text ‹This code was taken from IsaFoR. However, for the AFP, we use the version name \<^text>‹AFP›,
instead of a mercurial version. ›
local_setup ‹
  let
    val version = "AFP"
  in
    Local_Theory.define
      ((\<^binding>‹version›, NoSyn),
        ((\<^binding>‹version_def›, []), HOLogic.mk_literal version)) #> #2
  end
›

declare version_def [code]

end