From b1f331a5e7a641e4a9c5652e78a869884717be33 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 23 Jul 2024 09:29:41 +1000 Subject: [PATCH] [squash] locale requalify inside locale context example --- lib/test/Requalify_Test.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/test/Requalify_Test.thy b/lib/test/Requalify_Test.thy index 2015a1dcf9..ec29c9675c 100644 --- a/lib/test/Requalify_Test.thy +++ b/lib/test/Requalify_Test.thy @@ -72,10 +72,10 @@ requalify_consts (in Requalify_Example2) Requalify_Example1.ex1_const requalify_facts (in Requalify_Example2) Requalify_Example1.ex1_const_def (* this is equivalent to doing the requalifications in the locale context *) -context Requalify_Example2 begin -requalify_types (in Requalify_Example2) Requalify_Example1.ex1_type -requalify_consts (in Requalify_Example2) Requalify_Example1.ex1_const -requalify_facts (in Requalify_Example2) Requalify_Example1.ex1_const_def +context Requalify_Example1 begin +requalify_types (in Requalify_Example2) ex1_type +requalify_consts (in Requalify_Example2) ex1_const +requalify_facts (in Requalify_Example2) ex1_const_def end typ Requalify_Example2.ex1_type