src/Tools/isac/calcelems.sml
changeset 59550 2e7631381921
parent 59540 98298342fb6d
child 59562 d50fe358f04a
     1.1 --- a/src/Tools/isac/calcelems.sml	Sat Jun 01 11:09:19 2019 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Jun 22 13:15:52 2019 +0200
     1.3 @@ -614,7 +614,7 @@
     1.4          copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
     1.5          see ME/calchead.sml 'fun is_copy_named'.                                     *)
     1.6        pre        : term list,       (* preconditions in where                        *)
     1.7 -      scr        : Rule.scr         (* prep_met gets progam or string "empty_script" *)
     1.8 +      scr        : Rule.scr         (* progam, empty as @{thm refl} or Rfuns         *)
     1.9  	   };
    1.10  val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'",
    1.11  	erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls,