diff --git a/Citadelle/src/compiler_generic/toy_example/document_generated/Design_generated_generated.thy b/Citadelle/src/compiler_generic/toy_example/document_generated/Design_generated_generated.thy index 14032fd6c6c41ee0b7606f57f88e351925acc9bc..7a9bc2231b197d04732fb5d66c19278d366e1cb8 100644 --- a/Citadelle/src/compiler_generic/toy_example/document_generated/Design_generated_generated.thy +++ b/Citadelle/src/compiler_generic/toy_example/document_generated/Design_generated_generated.thy @@ -264,6 +264,10 @@ by(rule \<sigma>\<^sub>1) interpretation state_\<sigma>\<^sub>1': state_\<sigma>\<^sub>1' "oid1" "oid2" "oid3" "oid8" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n" "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4" by(rule \<sigma>\<^sub>1') + +definition "heap_\<sigma>\<^sub>1 = (heap (state_\<sigma>\<^sub>1.\<sigma>\<^sub>1))" + +definition "heap_\<sigma>\<^sub>1' = (heap (state_\<sigma>\<^sub>1'.\<sigma>\<^sub>1'))" end end