src/Tools/isac/Knowledge/Base_Tools.thy
changeset 60077 bd5be37901f8
parent 59910 778899c624a6
child 60149 f01072d28542
     1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Oct 05 12:05:10 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Oct 05 12:16:16 2020 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  theory Base_Tools
     1.5 -  imports  "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"
     1.6 -                                                          (*  ^^^ for KEStore_Elems.add_thes *)
     1.7 +  imports  Interpret.Interpret "../BridgeLibisabelle/BridgeLibisabelle"
     1.8 +                                (*  ^^^ for KEStore_Elems.add_thes *)
     1.9  begin
    1.10  subsection \<open>theorems for Base_Tools\<close>
    1.11  axiomatization where (*for evaluating the assumptions of conditional rules*)
    1.12 @@ -146,4 +146,4 @@
    1.13  setup \<open>KEStore_Elems.add_rlss
    1.14    [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end