test/Tools/isac/Specify/input-descript.sml
changeset 59959 0f0718c61f68
parent 59953 933211a252f2
child 60309 70a1d102660d
     1.1 --- a/test/Tools/isac/Specify/input-descript.sml	Sun May 10 15:55:30 2020 +0200
     1.2 +++ b/test/Tools/isac/Specify/input-descript.sml	Sun May 10 17:26:36 2020 +0200
     1.3 @@ -5,15 +5,15 @@
     1.4  "----------------------------------------------------------------------------------------------";
     1.5  "table of contents ----------------------------------------------------------------------------";
     1.6  "----------------------------------------------------------------------------------------------";
     1.7 -"-------- distinguish input to Model ----------------------------------------------------------";
     1.8 +"-------- distinguish input to I_Model --------------------------------------------------------";
     1.9  "----------------------------------------------------------------------------------------------";
    1.10  "----------------------------------------------------------------------------------------------";
    1.11  "----------------------------------------------------------------------------------------------";
    1.12  
    1.13  
    1.14 -"-------- distinguish input to Model ----------------------------------------------------------";
    1.15 -"-------- distinguish input to Model ----------------------------------------------------------";
    1.16 -"-------- distinguish input to Model ----------------------------------------------------------";
    1.17 +"-------- distinguish input to I_Model --------------------------------------------------------";
    1.18 +"-------- distinguish input to I_Model --------------------------------------------------------";
    1.19 +"-------- distinguish input to I_Model --------------------------------------------------------";
    1.20  "----- fun Input_Descript.for_bool_list -----";
    1.21  val t as Const ("Input_Descript.relations", 
    1.22    Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]),