Skip to content

Commit

Permalink
[squash] locale requalify inside locale context example
Browse files Browse the repository at this point in the history
  • Loading branch information
Xaphiosis committed Jul 23, 2024
1 parent b353544 commit 14a8536
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions lib/test/Requalify_Test.thy
Original file line number Diff line number Diff line change
Expand Up @@ -71,11 +71,11 @@ 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

(* 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
(* this is equivalent to doing the requalifications in the original locale context *)
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

Check failure on line 81 in lib/test/Requalify_Test.thy

View workflow job for this annotation

GitHub Actions / File annotations for theory linter

Interactive diagnostic command

This command is usually used interactively only and should only be checked in for demonstration purposes.
Expand Down

0 comments on commit 14a8536

Please sign in to comment.