test/Tools/isac/Test_Some.thy
changeset 59874 820bf0840029
parent 59866 3b194392ea71
child 59878 3163e63a5111
     1.1 --- a/test/Tools/isac/Test_Some.thy	Mon Apr 13 18:37:24 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Tue Apr 14 12:39:26 2020 +0200
     1.3 @@ -43,8 +43,8 @@
     1.4    open ContextC;               transfer_asms_from_to;
     1.5    open Tactic;                 (* NONE *)
     1.6    open Model;                  (* NONE *)
     1.7 -  open Rewrite;                mk_thm;
     1.8 -  open Num_Calc;                   get_pair;
     1.9 +  open Rewrite;
    1.10 +  open Num_Calc;               get_pair;
    1.11    open TermC;                  atomt;
    1.12    open Celem;                  e_pbt;
    1.13    open Rule;