Remove quick_and_dirty from operations

Author: jvanbruegge

operations/Composition.thy

@@ -34,7 +34,6 @@ val name2 = "T2";
 val rel = [[1,3], [1]];
 \<close>
 
-declare [[quick_and_dirty]]
 declare [[ML_print_depth=1000]]
 declare [[mrbnf_internals]]
 local_setup \<open>fn lthy =>
@@ -85,6 +84,4 @@ in lthy end
 print_theorems
 print_mrbnfs
 
-declare [[quick_and_dirty=false]]
-
 end

operations/Greatest_Fixpoint.thy

@@ -25,7 +25,6 @@ ML \<open>
   val rel = [[([], [0]), ([], [0, 1])]];
   \<close>
 
-declare [[quick_and_dirty]]
 declare [[ML_print_depth=1000]]
 declare [[mrbnf_internals]]
 local_setup \<open>fn lthy =>
@@ -62,8 +61,6 @@ set3_term_pre := recursive occurences that bind variables
 set4_term_pre := recursive non-binding occurences
 *)
 
-declare [[quick_and_dirty=false]]
-
 lemmas infinite_UNIV = cinfinite_imp_infinite[OF term_pre.UNIV_cinfinite]
 
 (********************** BINDER FIXPOINT CONSTRUCTION **************************************)
@@ -1809,4 +1806,4 @@ let
 in lthy end
 \<close>
 
-end
+end

operations/Least_Fixpoint2.thy

@@ -25,7 +25,6 @@ val name1 = "term";
 val rel = [[([], [0]), ([], [0, 1])]];
 \<close>
 
-declare [[quick_and_dirty]]
 declare [[ML_print_depth=1000]]
 declare [[mrbnf_internals]]
 local_setup \<open>fn lthy =>
@@ -56,8 +55,6 @@ in lthy end
 print_theorems
 print_mrbnfs
 
-declare [[quick_and_dirty=false]]
-
 lemmas infinite_UNIV = cinfinite_imp_infinite[OF term_pre.UNIV_cinfinite]
 
 (********************** BINDER FIXPOINT CONSTRUCTION **************************************)
@@ -2268,4 +2265,4 @@ lemma nnoclash_noclashs:
   apply (rule refl)
   done
 
-end
+end