Remove operation theories

Not relevant for POPL

Author: jvanbruegge

README.md

@@ -36,7 +36,6 @@ session | description
 Isabelle_Prelim|administrative session bundling standard Isabelle libraries we use
 Prelim|miscellaneous extensions to standard libraries, and bindings-specific infrastructure (e.g., countable and uncountable types we use for variables)
 Binders|main metatheory including the formalization our Thms 19 (called strong_induct in the formalization) and 22 (BE_iinduct) in Generic_Barendregt_Enhanced_Rule_Induction (Sect 4, 7.3, 8.2, 8.4 and App. G.2), the proof that our results generalize existing results from the literature in Urban_Berghofer_Norrish_Rule_Induction (App. A), and the binding-aware datatype automation in MRBNF_Composition and MRBNF_Recursor and the various ML files, App. G)
-Operations|detailed proof examples for automation of the metatheory
 Untyped_Lambda_Calculus|formalization of the untyped lambda calculus including beta reduction and parallel beta reduction (Sect 2)
 Process_Calculus|formalization of the pi calculus transition relation and the  associated strong rule induction principle (Sect 7.1 and App. D.3)
 System_Fsub|formalization of System F with subtyping, the associated strong rule induction principles, and the POPLmark challenge 1A, (Sect 7.2 and App. F)

ROOT

@@ -38,15 +38,6 @@ session Binders in "thys" = Prelim +
     General_Customization
     Urban_Berghofer_Norrish_Rule_Induction
 
-session Operations in "operations" = Untyped_Lambda_Calculus +
-  theories
-    Binder_Inductive
-    Fixpoint
-    Recursor
-    VVSubst
-    TVSubst
-    Sugar
-
 session Untyped_Lambda_Calculus in "thys/Untyped_Lambda_Calculus" = Binders +
   theories
     LC