Theory EPAC_Version

 (*
  File:         PAC_Version.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory EPAC_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 =
      trim_line (#1 (Isabelle_System.bash_output ("cd $ISAFOL/ && git rev-parse --short HEAD || echo unknown")))
  in
    Local_Theory.define
      ((binding‹version›, NoSyn),
        ((binding‹version_def›, []), HOLogic.mk_literal version)) #> #2
  end

declare version_def [code]

end