directory fdeep contains files using the definition of structures and formulae
as datatypes, whose constructors are the various connectives, as in GDC.thy ;

note that the fdeep development uses some files in common with ../gdeep,
these files are in ../cdeep

note that there are further changes, in cut-elimination proofs done for 
FILL - see directory ../fill, eg
types 'a pstructr (so structr = string pstructr)
sFind_def in terms of findf instead of previous,
with some consequential changes (eg thms "sFind.simps") 

Changes in fdeep from deep :

in fdeep a rule is a datatype with a single constructor,
and Bidi is a defined function (Bidi_def in RA_Rls.thy)

use of seqrep(s) and strrep instead of seqRep(s) and strRep

Hierarchy of theory files

Embedding to allow IsProvable
HOL_DL = List + 
  sequent structure formula rule
  stuff relating to provability
HOL_RS = HOL_DL +
  dRA structural operators

Full Deep Embedding, independent of actual calculus

stringSyntax = String
  to support parse and print translations for Structure and Formula variables
GDC = String + stringSyntax +
  formula, structr, sequent, rule as datatypes 
GSub = GDC + 
  stuff relating to substitution

GDT = GSub + 
  derivation tree as datatype, stuff relating to derivation trees,
  defines IsDerivableR as existence of a derivation tree ;
  inductive definition of derivableR using dtrel.thy, 
  by "derivableR ?rules == derrec (PC ` rulefs ?rules)" ;
  shows equivalence as IsDer_derR =
    "IsDerivableR ?rules ?prems ?concl = (?concl : derivableR ?rules ?prems)" 

  Then IsDerivableR_trans follows easily from derrec_trans (see DT1.ML)

GRep = GSub + 
  the replacement relation, used in cut-elimination
GCut = GRep + GDT + 
  stuff for cut-elimination, turning cuts into principal cuts
makeCut = GCut + GRep 

GElim = makeCut + 
  stuff for cut-elimination, turns results in other forms
  into results using canElim and canElimAll
  culminates in general cut-elimination theorem, 
  cutElim = "[| C345 ?rules; C8 ?rules; IsDerivableR ?rules {} ?concl |]
        ==> IsDerivableR (?rules - {cutr}) {} ?concl" : thm

stuff for relation algebras

RA_Syn = GDC + 
  syntax for relation algebras
RA_Ind = RA_Syn + GSub + 
  listing of rules - inductive style (RArls) ;
  proof of noNewSVs_rls_Ind - related to C4 - based on RArls
IDT = GDT + RA_Ind

RA_Rls = RA_Syn + GSub + 
  to do with rules (rls) and their properties, proves
  seqNoSSF_rls, noDupSVs_rls
RA_IR = RA_Rls + RA_Ind 
  relationship between rules and inductive-style rules
  RArls_fs = "RArls = PC ` rulefs rls" : thm
  proves noNewSVs_rls, noSVsAS_rls
  C345_rls = "C345 rls" : thm
RA_DT = RA_IR + GDT
  relating derivability using rls and RArls, IsDer_RArls =
    "IsDerivableR rls ?prems ?concl = (?concl : derrec RArls ?prems)" : thm

IDT = GDT + RA_Ind
  version of C8 using inductive-style rules RArls
ICut = GCut + IDT + RA_DT
  proves C8_rls = "C8 rls" : thm
IElim = GElim + ICut - culminates in cut-elimination theorem, RA_cutElim =
  "IsDerivableR rls {} ?concl ==> IsDerivableR (rls - {cutr}) {} ?concl" : thm 

HOL_C8 = GCut + RA_Rls 
  stuff for cut-elimination, procedures to prove Belnap C8 results,
  using deep-embedded rules (rls)
C8cases = HOL_C8 
RA_C8 = C8cases
  alternative proof of C8_rls 
RA_ElimC8 = GElim + RA_C8 + RA_IR 
  stuff for cut-elimination, putting HOL_C8 and GElim together

meta_proofs = GDT + RA_Rls
  ML code for construction of proof trees 
HOL_Disp = meta_proofs + RA_Rls +
  to do with displaying substructures

fdeep also contains extra definitions, needed for interpolation work,
in ../interp, which are not found in ../gdeep