Isabelle2018: InfoFlowC

proof/infoflow/ADT_IF_Refine.thy

@@ -9,8 +9,7 @@
  *)
 
 theory ADT_IF_Refine
-imports
-    "ADT_IF" "Refine.Refine" "Refine.EmptyFail_H"
+imports "InfoFlow.ADT_IF" "Refine.EmptyFail_H"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
@@ -1236,7 +1235,6 @@ lemma haskell_invs:
   supply conj_cong[cong]
   apply (unfold_locales)
                apply (simp add: ADT_H_if_def)
-               apply blast
               apply (simp_all add: checkActiveIRQ_H_if_def doUserOp_H_if_def
                                     kernelCall_H_if_def handlePreemption_H_if_def
                                     schedule'_H_if_def kernelExit_H_if_def split del: if_split)[12]

proof/infoflow/ADT_IF_Refine_C.thy

@@ -9,8 +9,7 @@
  *)
 
 theory ADT_IF_Refine_C
-imports
-    "ADT_IF_Refine" "CRefine.Refine_C"
+imports ADT_IF_Refine "CRefine.Refine_C"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
@@ -867,7 +866,6 @@ lemma c_to_haskell: "uop_nonempty uop \<Longrightarrow> global_automata_refine c
     apply (rule haskell_invs)
    apply (unfold_locales)
                         apply (simp add: ADT_C_if_def)
-                        apply blast
                        apply (simp_all add: preserves_trivial preserves'_trivial)
           apply (clarsimp simp: lift_snd_rel_def ADT_C_if_def ADT_H_if_def absKState_crelation
                                 rf_sr_def full_invs_if'_def)

proof/infoflow/Example_Valid_StateH.thy

@@ -9,9 +9,7 @@
  *)
 
 theory Example_Valid_StateH
-imports
-  Example_Valid_State
-  ADT_IF_Refine
+imports "InfoFlow.Example_Valid_State" ADT_IF_Refine
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)

proof/infoflow/Noninterference_Base_Refinement_Example.thy

@@ -9,8 +9,7 @@
  *)
 
 theory Noninterference_Base_Refinement_Example
-imports
-  Noninterference_Base_Refinement
+imports "InfoFlow.Noninterference_Base_Refinement"
 begin
 
 (* I don't like the 'refinedby' definition above.

proof/infoflow/Noninterference_Refinement.thy

@@ -9,7 +9,10 @@
  *)
 
 theory Noninterference_Refinement
-imports "Noninterference" "ADT_IF_Refine_C" "Noninterference_Base_Refinement"
+imports
+  "InfoFlow.Noninterference"
+  "ADT_IF_Refine_C"
+  "InfoFlow.Noninterference_Base_Refinement"
 begin
 
 (* FIXME: fp is currently ignored by ADT_C_if *)