Some LaTeX experiments with Achim

src/DOF/Isa_COL.thy

@@ -157,6 +157,9 @@ doc_class figure   =
    placement        :: placement  
    spawn_columns    :: bool <= True 
 
+doc_class figure2   =  figure +
+   caption          :: string
+
 
 doc_class side_by_side_figure = figure +
    anchor           :: "string"

src/tests/OutOfOrderPresntn.thy

@@ -504,7 +504,8 @@ Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
    \<close>  
 
 
-Figure*[ffff::figure,(* caption *) src="\<open>this is another 2 side-by-side\<close>"]
+
+Figure*[ffff::figure2, caption="\<open>this is another 2 side-by-side\<close>"]
    \<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "../ROOT"}\<close> 
    \<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "../ROOT"}\<close>  
 
@@ -512,5 +513,18 @@ Figure*[ffff::figure,(* caption *) src="\<open>this is another 2 side-by-side\<c
 text\<open> @{figure "ffff(2)"}\<close>
  *)
 
+Figure*[figxxx::figure2,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
+\<open>@{boxed_theory_text [display]
+\<open>lemma inv_c2_preserved :  "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
+  unfolding c1_inv_def c2_inv_def 
+            Computer_Hardware_to_Hardware_morphism_def
+            Product_to_Component_morphism_def  
+  by (auto simp: comp_def)
+
+lemma Computer_Hardware_to_Hardware_total :
+         "Computer_Hardware_to_Hardware_morphism ` ({X. c2_inv X}) 
+      \<subseteq> ({X::Hardware. c1_inv X})"
+  using inv_c2_preserved by auto\<close>}\<close> 
+
 end
 (*>*)