src/Tools/isac/Knowledge/Build_Thydata.thy
changeset 60608 5dabcc1c9235
parent 60588 9a116f94c5a6
child 60624 0e0ac7706f0d
     1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Sat Dec 03 19:12:38 2022 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Sun Dec 04 16:48:06 2022 +0100
     1.3 @@ -242,7 +242,7 @@
     1.4  insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
     1.5    (["chain-rule-diff-both", "cancel"]: errpatID list);
     1.6  [[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
     1.7 -  since Know_Store.set_ref_thy has been shifted below;
     1.8 +  since Know_Store.set_ref_last_thy has been shifted below;
     1.9    this ERROR will vanish during re-engineering towards Know_Store.]]]
    1.10  
    1.11     ...and all other related rls by hand;
    1.12 @@ -250,6 +250,6 @@
    1.13  \<close>
    1.14  
    1.15  section \<open>Link Know_Store to completed IsacKnowledge\<close>
    1.16 -ML \<open>Know_Store.set_ref_thy @{theory}\<close>
    1.17 +ML \<open>Know_Store.set_ref_last_thy @{theory}\<close>
    1.18  
    1.19  end