Note - the deep directory has largely been replaced by the files in the fdeep directory (and running them in Isabelle uses files in the cdeep directory, which contains stuff common to gdeep and fdeep) The Isabelle code doesn't seem to run any more - use fdeep instead 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 stringSyntax = String to support parse and print translations for Structure and Formula variables HOL_RA = String + stringSyntax + formula, structr, sequent, rule as datatypes HOL_Sub = HOL_RA + stuff relating to substitution HOL_Rls = HOL_Sub + to do with rules and their properties HOL_PT = HOL_Sub + pftree as datatype, stuff relating to proof trees HOL_Rep = HOL_Sub + the replacement relation, used in cut-elimination HOL_Cut = HOL_Rep + HOL_PT + HOL_Rls + stuff for cut-elimination, turning cuts into principal cuts HOL_Elim = HOL_Cut + stuff for cut-elimination, turns results in other forms into results using canElim and canElimAll HOL_C8 = HOL_Cut stuff for cut-elimination, procedures to prove Belnap C8 results HOL_ElimC8 = HOL_Elim + HOL_C8 stuff for cut-elimination, putting HOL_C8 and HOL_Elim together meta_proofs = HOL_PT + HOL_Rls ML code for construction of proof trees HOL_Disp = meta_proofs + HOL_Rls + to do with displaying substructures