test/Tools/isac/Test_Isac_Short.thy
changeset 60336 dcb37736d573
parent 60330 e5e9a6c45597
child 60337 cbad4e18e91b
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4    -------------------------------------------------------------------------ARE AT THE RIGHT MARGIN*)
     1.5  section \<open>trials with Isabelle's functions\<close>
     1.6    ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
     1.7 -  ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
     1.8 +  ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML" 
     1.9    ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
    1.10    ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
    1.11    ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
    1.12 @@ -329,7 +329,9 @@
    1.13    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.14  ML \<open>
    1.15  \<close> ML \<open>
    1.16 +@{term Let}
    1.17  \<close> ML \<open>
    1.18 +val Const (\<^const_name>\<open>Let\<close>, _) = @{term Let}
    1.19  \<close> ML \<open>
    1.20  \<close> ML \<open>
    1.21  \<close> ML \<open>