Theory Ids

theory "Ids"
imports Complex_Main
  "Syntax"
begin
text ‹Some specific identifiers used in Axioms›
abbreviation hgid1::ident where "hgid1 ≡ CHR ''a''"
abbreviation hgid2::ident where "hgid2 ≡ CHR ''b''"
abbreviation hgidc::ident where "hgidc ≡ CHR ''c''"
abbreviation hgidd::ident where "hgidd ≡ CHR ''d''"
abbreviation pid1::ident  where "pid1  ≡ CHR ''p''"
abbreviation pid2::ident  where "pid2  ≡ CHR ''q''"
abbreviation fid1::ident  where "fid1  ≡ CHR ''f''"
abbreviation xid1::variable where "xid1  ≡ RVar (CHR ''x'')"
end