From bde97113ad0b1ba99caf8149e447d6256a9c6932 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?= <tuong@users.noreply.github.com> Date: Tue, 5 May 2020 19:57:30 +0000 Subject: [PATCH] update the generated files git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14177 3260e6d1-4efc-4170-b0a7-36055960796d --- .../document_generated/Design_generated_generated.thy | 4 ++++ 1 file changed, 4 insertions(+) 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 14032fd6c6c..7a9bc2231b1 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 -- GitLab