isabelle update -u path_cartouches;
authorwenzelm
Sun Jan 06 15:04:34 2019 +0100 (4 months ago)
changeset 69605a96320074298
parent 69604 d80b2df54d31
child 69606 157990515be1
isabelle update -u path_cartouches;
src/CTT/CTT.thy
src/Doc/Classes/Setup.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Setup.thy
src/Doc/Datatypes/Setup.thy
src/Doc/Eisbach/Base.thy
src/Doc/Implementation/Base.thy
src/Doc/Isar_Ref/Base.thy
src/Doc/JEdit/Base.thy
src/Doc/Logics_ZF/ZF_Isar.thy
src/Doc/System/Base.thy
src/Doc/Tutorial/Inductive/Advanced.thy
src/Doc/Tutorial/Inductive/Even.thy
src/Doc/Tutorial/Protocol/Message.thy
src/Doc/Tutorial/Types/Setup.thy
src/Doc/Typeclass_Hierarchy/Setup.thy
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/FOLP/FOLP.thy
src/FOLP/IFOLP.thy
src/HOL/ATP.thy
src/HOL/Algebra/Ring.thy
src/HOL/Analysis/Measurable.thy
src/HOL/Analysis/Norm_Arith.thy
src/HOL/Argo.thy
src/HOL/BNF_Composition.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Basic_BNF_LFPs.thy
src/HOL/Code_Evaluation.thy
src/HOL/Ctr_Sugar.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Eisbach/Eisbach.thy
src/HOL/Extraction.thy
src/HOL/Fields.thy
src/HOL/Fun.thy
src/HOL/Fun_Def.thy
src/HOL/Fun_Def_Base.thy
src/HOL/Groebner_Basis.thy
src/HOL/Groups.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Import/Import_Setup.thy
src/HOL/Inductive.thy
src/HOL/Int.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Lattices.thy
src/HOL/Library/Adhoc_Overloading.thy
src/HOL/Library/BNF_Axiomatization.thy
src/HOL/Library/BNF_Corec.thy
src/HOL/Library/Cancellation.thy
src/HOL/Library/Case_Converter.thy
src/HOL/Library/Code_Lazy.thy
src/HOL/Library/Code_Prolog.thy
src/HOL/Library/Code_Test.thy
src/HOL/Library/Conditional_Parametricity.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Datatype_Records.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/Library/Realizers.thy
src/HOL/Library/Reflection.thy
src/HOL/Library/Refute.thy
src/HOL/Library/Rewrite.thy
src/HOL/Library/Simps_Case_Conv.thy
src/HOL/Library/Sum_of_Squares.thy
src/HOL/Lifting.thy
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
src/HOL/Matrix_LP/Cplex.thy
src/HOL/Meson.thy
src/HOL/Metis.thy
src/HOL/Mirabelle/Mirabelle.thy
src/HOL/Mirabelle/Mirabelle_Test.thy
src/HOL/Mutabelle/MutabelleExtra.thy
src/HOL/Nat.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Num.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Nunchaku.thy
src/HOL/Orderings.thy
src/HOL/Partial_Function.thy
src/HOL/Predicate_Compile.thy
src/HOL/Presburger.thy
src/HOL/Product_Type.thy
src/HOL/Prolog/HOHH.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Quotient.thy
src/HOL/Real.thy
src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy
src/HOL/Record.thy
src/HOL/Rings.thy
src/HOL/SAT.thy
src/HOL/SMT.thy
src/HOL/SMT_Examples/Boogie.thy
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
src/HOL/SPARK/Examples/RIPEMD-160/F.thy
src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy
src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy
src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy
src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy
src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy
src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy
src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy
src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
src/HOL/SPARK/Manual/Complex_Types.thy
src/HOL/SPARK/Manual/Proc1.thy
src/HOL/SPARK/Manual/Proc2.thy
src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
src/HOL/SPARK/SPARK_Setup.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Sledgehammer.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/String.thy
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/ATP_Theory_Export.thy
src/HOL/TPTP/MaSh_Eval.thy
src/HOL/TPTP/MaSh_Export_Base.thy
src/HOL/TPTP/TPTP_Interpret.thy
src/HOL/TPTP/TPTP_Parser.thy
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/HOL/Transfer.thy
src/HOL/Transitive_Closure.thy
src/HOL/Typedef.thy
src/HOL/Types_To_Sets/Types_To_Sets.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/Word/Word.thy
src/Sequents/LK.thy
src/Sequents/Modal0.thy
src/Sequents/Sequents.thy
src/Tools/Code_Generator.thy
src/Tools/SML/Examples.thy
src/Tools/Spec_Check/Spec_Check.thy
src/ZF/ArithSimp.thy
src/ZF/Bin.thy
src/ZF/Datatype.thy
src/ZF/Inductive.thy
src/ZF/pair.thy
src/ZF/upair.thy
     1.1 --- a/src/CTT/CTT.thy	Sun Jan 06 13:44:33 2019 +0100
     1.2 +++ b/src/CTT/CTT.thy	Sun Jan 06 15:04:34 2019 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  section \<open>Constructive Type Theory: axiomatic basis\<close>
     1.6  
     1.7 -ML_file "~~/src/Provers/typedsimp.ML"
     1.8 +ML_file \<open>~~/src/Provers/typedsimp.ML\<close>
     1.9  setup Pure_Thy.old_appl_syntax_setup
    1.10  
    1.11  typedecl i
    1.12 @@ -455,7 +455,7 @@
    1.13  method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close>
    1.14  method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close>
    1.15  
    1.16 -ML_file "rew.ML"
    1.17 +ML_file \<open>rew.ML\<close>
    1.18  method_setup rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))\<close>
    1.19  method_setup hyp_rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))\<close>
    1.20  
     2.1 --- a/src/Doc/Classes/Setup.thy	Sun Jan 06 13:44:33 2019 +0100
     2.2 +++ b/src/Doc/Classes/Setup.thy	Sun Jan 06 15:04:34 2019 +0100
     2.3 @@ -2,8 +2,8 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -ML_file "../antiquote_setup.ML"
     2.8 -ML_file "../more_antiquote.ML"
     2.9 +ML_file \<open>../antiquote_setup.ML\<close>
    2.10 +ML_file \<open>../more_antiquote.ML\<close>
    2.11  
    2.12  declare [[default_code_width = 74]]
    2.13  
     3.1 --- a/src/Doc/Codegen/Introduction.thy	Sun Jan 06 13:44:33 2019 +0100
     3.2 +++ b/src/Doc/Codegen/Introduction.thy	Sun Jan 06 15:04:34 2019 +0100
     3.3 @@ -69,7 +69,7 @@
     3.4  text \<open>\noindent Then we can generate code e.g.~for \<open>SML\<close> as follows:\<close>
     3.5  
     3.6  export_code %quote empty dequeue enqueue in SML
     3.7 -  module_name Example file "$ISABELLE_TMP/example.ML"
     3.8 +  module_name Example file \<open>$ISABELLE_TMP/example.ML\<close>
     3.9  
    3.10  text \<open>\noindent resulting in the following code:\<close>
    3.11  
    3.12 @@ -90,7 +90,7 @@
    3.13  \<close>
    3.14  
    3.15  export_code %quote empty dequeue enqueue in Haskell
    3.16 -  module_name Example file "$ISABELLE_TMP/examples/"
    3.17 +  module_name Example file \<open>$ISABELLE_TMP/examples/\<close>
    3.18  
    3.19  text \<open>
    3.20    \noindent This is the corresponding code:
     4.1 --- a/src/Doc/Codegen/Setup.thy	Sun Jan 06 13:44:33 2019 +0100
     4.2 +++ b/src/Doc/Codegen/Setup.thy	Sun Jan 06 15:04:34 2019 +0100
     4.3 @@ -7,8 +7,8 @@
     4.4    "HOL-Library.IArray"
     4.5  begin
     4.6  
     4.7 -ML_file "../antiquote_setup.ML"
     4.8 -ML_file "../more_antiquote.ML"
     4.9 +ML_file \<open>../antiquote_setup.ML\<close>
    4.10 +ML_file \<open>../more_antiquote.ML\<close>
    4.11  
    4.12  no_syntax (output)
    4.13    "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
     5.1 --- a/src/Doc/Datatypes/Setup.thy	Sun Jan 06 13:44:33 2019 +0100
     5.2 +++ b/src/Doc/Datatypes/Setup.thy	Sun Jan 06 15:04:34 2019 +0100
     5.3 @@ -2,6 +2,6 @@
     5.4  imports Main
     5.5  begin
     5.6  
     5.7 -ML_file "../antiquote_setup.ML"
     5.8 +ML_file \<open>../antiquote_setup.ML\<close>
     5.9  
    5.10  end
     6.1 --- a/src/Doc/Eisbach/Base.thy	Sun Jan 06 13:44:33 2019 +0100
     6.2 +++ b/src/Doc/Eisbach/Base.thy	Sun Jan 06 15:04:34 2019 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  imports Main
     6.5  begin
     6.6  
     6.7 -ML_file "~~/src/Doc/antiquote_setup.ML"
     6.8 +ML_file \<open>~~/src/Doc/antiquote_setup.ML\<close>
     6.9  
    6.10  ML\<open>
    6.11  fun get_split_rule ctxt target =
     7.1 --- a/src/Doc/Implementation/Base.thy	Sun Jan 06 13:44:33 2019 +0100
     7.2 +++ b/src/Doc/Implementation/Base.thy	Sun Jan 06 15:04:34 2019 +0100
     7.3 @@ -4,6 +4,6 @@
     7.4  imports Main
     7.5  begin
     7.6  
     7.7 -ML_file "../antiquote_setup.ML"
     7.8 +ML_file \<open>../antiquote_setup.ML\<close>
     7.9  
    7.10  end
     8.1 --- a/src/Doc/Isar_Ref/Base.thy	Sun Jan 06 13:44:33 2019 +0100
     8.2 +++ b/src/Doc/Isar_Ref/Base.thy	Sun Jan 06 15:04:34 2019 +0100
     8.3 @@ -4,6 +4,6 @@
     8.4  imports Pure
     8.5  begin
     8.6  
     8.7 -ML_file "../antiquote_setup.ML"
     8.8 +ML_file \<open>../antiquote_setup.ML\<close>
     8.9  
    8.10  end
     9.1 --- a/src/Doc/JEdit/Base.thy	Sun Jan 06 13:44:33 2019 +0100
     9.2 +++ b/src/Doc/JEdit/Base.thy	Sun Jan 06 15:04:34 2019 +0100
     9.3 @@ -4,6 +4,6 @@
     9.4  imports Main
     9.5  begin
     9.6  
     9.7 -ML_file "../antiquote_setup.ML"
     9.8 +ML_file \<open>../antiquote_setup.ML\<close>
     9.9  
    9.10  end
    10.1 --- a/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 06 13:44:33 2019 +0100
    10.2 +++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 06 15:04:34 2019 +0100
    10.3 @@ -3,7 +3,7 @@
    10.4  begin
    10.5  
    10.6  (*<*)
    10.7 -ML_file "../antiquote_setup.ML"
    10.8 +ML_file \<open>../antiquote_setup.ML\<close>
    10.9  (*>*)
   10.10  
   10.11  chapter \<open>Some Isar language elements\<close>
    11.1 --- a/src/Doc/System/Base.thy	Sun Jan 06 13:44:33 2019 +0100
    11.2 +++ b/src/Doc/System/Base.thy	Sun Jan 06 15:04:34 2019 +0100
    11.3 @@ -4,6 +4,6 @@
    11.4  imports Pure
    11.5  begin
    11.6  
    11.7 -ML_file "../antiquote_setup.ML"
    11.8 +ML_file \<open>../antiquote_setup.ML\<close>
    11.9  
   11.10  end
    12.1 --- a/src/Doc/Tutorial/Inductive/Advanced.thy	Sun Jan 06 13:44:33 2019 +0100
    12.2 +++ b/src/Doc/Tutorial/Inductive/Advanced.thy	Sun Jan 06 15:04:34 2019 +0100
    12.3 @@ -1,5 +1,5 @@
    12.4  (*<*)theory Advanced imports Even begin
    12.5 -ML_file "../../antiquote_setup.ML"
    12.6 +ML_file \<open>../../antiquote_setup.ML\<close>
    12.7  (*>*)
    12.8  
    12.9  text \<open>
    13.1 --- a/src/Doc/Tutorial/Inductive/Even.thy	Sun Jan 06 13:44:33 2019 +0100
    13.2 +++ b/src/Doc/Tutorial/Inductive/Even.thy	Sun Jan 06 15:04:34 2019 +0100
    13.3 @@ -1,5 +1,5 @@
    13.4  (*<*)theory Even imports Main begin
    13.5 -ML_file "../../antiquote_setup.ML" 
    13.6 +ML_file \<open>../../antiquote_setup.ML\<close> 
    13.7  (*>*)
    13.8  
    13.9  section\<open>The Set of Even Numbers\<close>
    14.1 --- a/src/Doc/Tutorial/Protocol/Message.thy	Sun Jan 06 13:44:33 2019 +0100
    14.2 +++ b/src/Doc/Tutorial/Protocol/Message.thy	Sun Jan 06 15:04:34 2019 +0100
    14.3 @@ -8,7 +8,7 @@
    14.4  section\<open>Theory of Agents and Messages for Security Protocols\<close>
    14.5  
    14.6  theory Message imports Main begin
    14.7 -ML_file "../../antiquote_setup.ML"
    14.8 +ML_file \<open>../../antiquote_setup.ML\<close>
    14.9  
   14.10  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   14.11  lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
    15.1 --- a/src/Doc/Tutorial/Types/Setup.thy	Sun Jan 06 13:44:33 2019 +0100
    15.2 +++ b/src/Doc/Tutorial/Types/Setup.thy	Sun Jan 06 15:04:34 2019 +0100
    15.3 @@ -2,7 +2,7 @@
    15.4  imports Main
    15.5  begin
    15.6  
    15.7 -ML_file "../../antiquote_setup.ML"
    15.8 -ML_file "../../more_antiquote.ML"
    15.9 +ML_file \<open>../../antiquote_setup.ML\<close>
   15.10 +ML_file \<open>../../more_antiquote.ML\<close>
   15.11  
   15.12  end
    16.1 --- a/src/Doc/Typeclass_Hierarchy/Setup.thy	Sun Jan 06 13:44:33 2019 +0100
    16.2 +++ b/src/Doc/Typeclass_Hierarchy/Setup.thy	Sun Jan 06 15:04:34 2019 +0100
    16.3 @@ -2,8 +2,8 @@
    16.4  imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
    16.5  begin
    16.6  
    16.7 -ML_file "../antiquote_setup.ML"
    16.8 -ML_file "../more_antiquote.ML"
    16.9 +ML_file \<open>../antiquote_setup.ML\<close>
   16.10 +ML_file \<open>../more_antiquote.ML\<close>
   16.11  
   16.12  attribute_setup all =
   16.13    \<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
    17.1 --- a/src/FOL/FOL.thy	Sun Jan 06 13:44:33 2019 +0100
    17.2 +++ b/src/FOL/FOL.thy	Sun Jan 06 15:04:34 2019 +0100
    17.3 @@ -9,9 +9,9 @@
    17.4  keywords "print_claset" "print_induct_rules" :: diag
    17.5  begin
    17.6  
    17.7 -ML_file "~~/src/Provers/classical.ML"
    17.8 -ML_file "~~/src/Provers/blast.ML"
    17.9 -ML_file "~~/src/Provers/clasimp.ML"
   17.10 +ML_file \<open>~~/src/Provers/classical.ML\<close>
   17.11 +ML_file \<open>~~/src/Provers/blast.ML\<close>
   17.12 +ML_file \<open>~~/src/Provers/clasimp.ML\<close>
   17.13  
   17.14  
   17.15  subsection \<open>The classical axiom\<close>
   17.16 @@ -335,7 +335,7 @@
   17.17    not_imp not_all not_ex cases_simp cla_simps_misc
   17.18  
   17.19  
   17.20 -ML_file "simpdata.ML"
   17.21 +ML_file \<open>simpdata.ML\<close>
   17.22  
   17.23  simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close>
   17.24  simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close>
   17.25 @@ -361,7 +361,7 @@
   17.26    Simplifier.method_setup Splitter.split_modifiers
   17.27  \<close>
   17.28  
   17.29 -ML_file "~~/src/Tools/eqsubst.ML"
   17.30 +ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
   17.31  
   17.32  
   17.33  subsection \<open>Other simple lemmas\<close>
   17.34 @@ -429,7 +429,7 @@
   17.35  
   17.36  text \<open>Method setup.\<close>
   17.37  
   17.38 -ML_file "~~/src/Tools/induct.ML"
   17.39 +ML_file \<open>~~/src/Tools/induct.ML\<close>
   17.40  ML \<open>
   17.41    structure Induct = Induct
   17.42    (
   17.43 @@ -447,7 +447,7 @@
   17.44  
   17.45  end
   17.46  
   17.47 -ML_file "~~/src/Tools/case_product.ML"
   17.48 +ML_file \<open>~~/src/Tools/case_product.ML\<close>
   17.49  
   17.50  
   17.51  hide_const (open) eq
    18.1 --- a/src/FOL/IFOL.thy	Sun Jan 06 13:44:33 2019 +0100
    18.2 +++ b/src/FOL/IFOL.thy	Sun Jan 06 15:04:34 2019 +0100
    18.3 @@ -9,16 +9,16 @@
    18.4  begin
    18.5  
    18.6  ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
    18.7 -ML_file "~~/src/Tools/misc_legacy.ML"
    18.8 -ML_file "~~/src/Provers/splitter.ML"
    18.9 -ML_file "~~/src/Provers/hypsubst.ML"
   18.10 -ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
   18.11 -ML_file "~~/src/Tools/IsaPlanner/isand.ML"
   18.12 -ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
   18.13 -ML_file "~~/src/Provers/quantifier1.ML"
   18.14 -ML_file "~~/src/Tools/intuitionistic.ML"
   18.15 -ML_file "~~/src/Tools/project_rule.ML"
   18.16 -ML_file "~~/src/Tools/atomize_elim.ML"
   18.17 +ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
   18.18 +ML_file \<open>~~/src/Provers/splitter.ML\<close>
   18.19 +ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
   18.20 +ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
   18.21 +ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
   18.22 +ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
   18.23 +ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
   18.24 +ML_file \<open>~~/src/Tools/intuitionistic.ML\<close>
   18.25 +ML_file \<open>~~/src/Tools/project_rule.ML\<close>
   18.26 +ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
   18.27  
   18.28  
   18.29  subsection \<open>Syntax and axiomatic basis\<close>
   18.30 @@ -582,7 +582,7 @@
   18.31  )
   18.32  \<close>
   18.33  
   18.34 -ML_file "fologic.ML"
   18.35 +ML_file \<open>fologic.ML\<close>
   18.36  
   18.37  lemma thin_refl: \<open>\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W\<close> .
   18.38  
   18.39 @@ -603,7 +603,7 @@
   18.40  open Hypsubst;
   18.41  \<close>
   18.42  
   18.43 -ML_file "intprover.ML"
   18.44 +ML_file \<open>intprover.ML\<close>
   18.45  
   18.46  
   18.47  subsection \<open>Intuitionistic Reasoning\<close>
    19.1 --- a/src/FOLP/FOLP.thy	Sun Jan 06 13:44:33 2019 +0100
    19.2 +++ b/src/FOLP/FOLP.thy	Sun Jan 06 15:04:34 2019 +0100
    19.3 @@ -98,8 +98,8 @@
    19.4    apply assumption
    19.5    done
    19.6  
    19.7 -ML_file "classical.ML"      (* Patched because matching won't instantiate proof *)
    19.8 -ML_file "simp.ML"           (* Patched because matching won't instantiate proof *)
    19.9 +ML_file \<open>classical.ML\<close>      (* Patched because matching won't instantiate proof *)
   19.10 +ML_file \<open>simp.ML\<close>           (* Patched because matching won't instantiate proof *)
   19.11  
   19.12  ML \<open>
   19.13  structure Cla = Classical
   19.14 @@ -138,6 +138,6 @@
   19.15    apply (tactic \<open>ALLGOALS (Cla.fast_tac \<^context> FOLP_cs)\<close>)
   19.16    done
   19.17  
   19.18 -ML_file "simpdata.ML"
   19.19 +ML_file \<open>simpdata.ML\<close>
   19.20  
   19.21  end
    20.1 --- a/src/FOLP/IFOLP.thy	Sun Jan 06 13:44:33 2019 +0100
    20.2 +++ b/src/FOLP/IFOLP.thy	Sun Jan 06 15:04:34 2019 +0100
    20.3 @@ -9,7 +9,7 @@
    20.4  imports Pure
    20.5  begin
    20.6  
    20.7 -ML_file "~~/src/Tools/misc_legacy.ML"
    20.8 +ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
    20.9  
   20.10  setup Pure_Thy.old_appl_syntax_setup
   20.11  
   20.12 @@ -605,7 +605,7 @@
   20.13  
   20.14  lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
   20.15  
   20.16 -ML_file "hypsubst.ML"
   20.17 +ML_file \<open>hypsubst.ML\<close>
   20.18  
   20.19  ML \<open>
   20.20  structure Hypsubst = Hypsubst
   20.21 @@ -627,7 +627,7 @@
   20.22  open Hypsubst;
   20.23  \<close>
   20.24  
   20.25 -ML_file "intprover.ML"
   20.26 +ML_file \<open>intprover.ML\<close>
   20.27  
   20.28  
   20.29  (*** Rewrite rules ***)
    21.1 --- a/src/HOL/ATP.thy	Sun Jan 06 13:44:33 2019 +0100
    21.2 +++ b/src/HOL/ATP.thy	Sun Jan 06 15:04:34 2019 +0100
    21.3 @@ -11,11 +11,11 @@
    21.4  
    21.5  subsection \<open>ATP problems and proofs\<close>
    21.6  
    21.7 -ML_file "Tools/ATP/atp_util.ML"
    21.8 -ML_file "Tools/ATP/atp_problem.ML"
    21.9 -ML_file "Tools/ATP/atp_proof.ML"
   21.10 -ML_file "Tools/ATP/atp_proof_redirect.ML"
   21.11 -ML_file "Tools/ATP/atp_satallax.ML"
   21.12 +ML_file \<open>Tools/ATP/atp_util.ML\<close>
   21.13 +ML_file \<open>Tools/ATP/atp_problem.ML\<close>
   21.14 +ML_file \<open>Tools/ATP/atp_proof.ML\<close>
   21.15 +ML_file \<open>Tools/ATP/atp_proof_redirect.ML\<close>
   21.16 +ML_file \<open>Tools/ATP/atp_satallax.ML\<close>
   21.17  
   21.18  
   21.19  subsection \<open>Higher-order reasoning helpers\<close>
   21.20 @@ -146,12 +146,12 @@
   21.21  
   21.22  subsection \<open>Basic connection between ATPs and HOL\<close>
   21.23  
   21.24 -ML_file "Tools/lambda_lifting.ML"
   21.25 -ML_file "Tools/monomorph.ML"
   21.26 -ML_file "Tools/ATP/atp_problem_generate.ML"
   21.27 -ML_file "Tools/ATP/atp_proof_reconstruct.ML"
   21.28 -ML_file "Tools/ATP/atp_systems.ML"
   21.29 -ML_file "Tools/ATP/atp_waldmeister.ML"
   21.30 +ML_file \<open>Tools/lambda_lifting.ML\<close>
   21.31 +ML_file \<open>Tools/monomorph.ML\<close>
   21.32 +ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
   21.33 +ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
   21.34 +ML_file \<open>Tools/ATP/atp_systems.ML\<close>
   21.35 +ML_file \<open>Tools/ATP/atp_waldmeister.ML\<close>
   21.36  
   21.37  hide_fact (open) waldmeister_fol boolean_equality boolean_comm
   21.38  
    22.1 --- a/src/HOL/Algebra/Ring.thy	Sun Jan 06 13:44:33 2019 +0100
    22.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Jan 06 15:04:34 2019 +0100
    22.3 @@ -418,7 +418,7 @@
    22.4    compute distributive normal form in locale contexts\<close>
    22.5  
    22.6  
    22.7 -ML_file "ringsimp.ML"
    22.8 +ML_file \<open>ringsimp.ML\<close>
    22.9  
   22.10  attribute_setup algebra = \<open>
   22.11    Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
    23.1 --- a/src/HOL/Analysis/Measurable.thy	Sun Jan 06 13:44:33 2019 +0100
    23.2 +++ b/src/HOL/Analysis/Measurable.thy	Sun Jan 06 15:04:34 2019 +0100
    23.3 @@ -46,7 +46,7 @@
    23.4  lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
    23.5    by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
    23.6  
    23.7 -ML_file "measurable.ML"
    23.8 +ML_file \<open>measurable.ML\<close>
    23.9  
   23.10  attribute_setup measurable = \<open>
   23.11    Scan.lift (
    24.1 --- a/src/HOL/Analysis/Norm_Arith.thy	Sun Jan 06 13:44:33 2019 +0100
    24.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Sun Jan 06 15:04:34 2019 +0100
    24.3 @@ -129,7 +129,7 @@
    24.4    mult_1_left
    24.5    mult_1_right
    24.6  
    24.7 -ML_file "normarith.ML"
    24.8 +ML_file \<open>normarith.ML\<close>
    24.9  
   24.10  method_setup%important norm = \<open>
   24.11    Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
    25.1 --- a/src/HOL/Argo.thy	Sun Jan 06 13:44:33 2019 +0100
    25.2 +++ b/src/HOL/Argo.thy	Sun Jan 06 15:04:34 2019 +0100
    25.3 @@ -6,22 +6,22 @@
    25.4  imports HOL
    25.5  begin
    25.6  
    25.7 -ML_file "~~/src/Tools/Argo/argo_expr.ML"
    25.8 -ML_file "~~/src/Tools/Argo/argo_term.ML"
    25.9 -ML_file "~~/src/Tools/Argo/argo_lit.ML"
   25.10 -ML_file "~~/src/Tools/Argo/argo_proof.ML"
   25.11 -ML_file "~~/src/Tools/Argo/argo_rewr.ML"
   25.12 -ML_file "~~/src/Tools/Argo/argo_cls.ML"
   25.13 -ML_file "~~/src/Tools/Argo/argo_common.ML"
   25.14 -ML_file "~~/src/Tools/Argo/argo_cc.ML"
   25.15 -ML_file "~~/src/Tools/Argo/argo_simplex.ML"
   25.16 -ML_file "~~/src/Tools/Argo/argo_thy.ML"
   25.17 -ML_file "~~/src/Tools/Argo/argo_heap.ML"
   25.18 -ML_file "~~/src/Tools/Argo/argo_cdcl.ML"
   25.19 -ML_file "~~/src/Tools/Argo/argo_core.ML"
   25.20 -ML_file "~~/src/Tools/Argo/argo_clausify.ML"
   25.21 -ML_file "~~/src/Tools/Argo/argo_solver.ML"
   25.22 +ML_file \<open>~~/src/Tools/Argo/argo_expr.ML\<close>
   25.23 +ML_file \<open>~~/src/Tools/Argo/argo_term.ML\<close>
   25.24 +ML_file \<open>~~/src/Tools/Argo/argo_lit.ML\<close>
   25.25 +ML_file \<open>~~/src/Tools/Argo/argo_proof.ML\<close>
   25.26 +ML_file \<open>~~/src/Tools/Argo/argo_rewr.ML\<close>
   25.27 +ML_file \<open>~~/src/Tools/Argo/argo_cls.ML\<close>
   25.28 +ML_file \<open>~~/src/Tools/Argo/argo_common.ML\<close>
   25.29 +ML_file \<open>~~/src/Tools/Argo/argo_cc.ML\<close>
   25.30 +ML_file \<open>~~/src/Tools/Argo/argo_simplex.ML\<close>
   25.31 +ML_file \<open>~~/src/Tools/Argo/argo_thy.ML\<close>
   25.32 +ML_file \<open>~~/src/Tools/Argo/argo_heap.ML\<close>
   25.33 +ML_file \<open>~~/src/Tools/Argo/argo_cdcl.ML\<close>
   25.34 +ML_file \<open>~~/src/Tools/Argo/argo_core.ML\<close>
   25.35 +ML_file \<open>~~/src/Tools/Argo/argo_clausify.ML\<close>
   25.36 +ML_file \<open>~~/src/Tools/Argo/argo_solver.ML\<close>
   25.37  
   25.38 -ML_file "Tools/Argo/argo_tactic.ML"
   25.39 +ML_file \<open>Tools/Argo/argo_tactic.ML\<close>
   25.40  
   25.41  end
    26.1 --- a/src/HOL/BNF_Composition.thy	Sun Jan 06 13:44:33 2019 +0100
    26.2 +++ b/src/HOL/BNF_Composition.thy	Sun Jan 06 15:04:34 2019 +0100
    26.3 @@ -178,9 +178,9 @@
    26.4  lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
    26.5    unfolding id_bnf_def by unfold_locales auto
    26.6  
    26.7 -ML_file "Tools/BNF/bnf_comp_tactics.ML"
    26.8 -ML_file "Tools/BNF/bnf_comp.ML"
    26.9 -ML_file "Tools/BNF/bnf_lift.ML"
   26.10 +ML_file \<open>Tools/BNF/bnf_comp_tactics.ML\<close>
   26.11 +ML_file \<open>Tools/BNF/bnf_comp.ML\<close>
   26.12 +ML_file \<open>Tools/BNF/bnf_lift.ML\<close>
   26.13  
   26.14  hide_fact
   26.15    DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0
    27.1 --- a/src/HOL/BNF_Def.thy	Sun Jan 06 13:44:33 2019 +0100
    27.2 +++ b/src/HOL/BNF_Def.thy	Sun Jan 06 15:04:34 2019 +0100
    27.3 @@ -272,9 +272,9 @@
    27.4  lemma eq_onp_mono_iff: "eq_onp P \<le> eq_onp Q \<longleftrightarrow> P \<le> Q"
    27.5    unfolding eq_onp_def by auto
    27.6  
    27.7 -ML_file "Tools/BNF/bnf_util.ML"
    27.8 -ML_file "Tools/BNF/bnf_tactics.ML"
    27.9 -ML_file "Tools/BNF/bnf_def_tactics.ML"
   27.10 -ML_file "Tools/BNF/bnf_def.ML"
   27.11 +ML_file \<open>Tools/BNF/bnf_util.ML\<close>
   27.12 +ML_file \<open>Tools/BNF/bnf_tactics.ML\<close>
   27.13 +ML_file \<open>Tools/BNF/bnf_def_tactics.ML\<close>
   27.14 +ML_file \<open>Tools/BNF/bnf_def.ML\<close>
   27.15  
   27.16  end
    28.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Sun Jan 06 13:44:33 2019 +0100
    28.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Sun Jan 06 15:04:34 2019 +0100
    28.3 @@ -287,12 +287,12 @@
    28.4  lemma Let_const: "Let x (\<lambda>_. c) = c"
    28.5    unfolding Let_def ..
    28.6  
    28.7 -ML_file "Tools/BNF/bnf_fp_util_tactics.ML"
    28.8 -ML_file "Tools/BNF/bnf_fp_util.ML"
    28.9 -ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
   28.10 -ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
   28.11 -ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
   28.12 -ML_file "Tools/BNF/bnf_fp_n2m.ML"
   28.13 -ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
   28.14 +ML_file \<open>Tools/BNF/bnf_fp_util_tactics.ML\<close>
   28.15 +ML_file \<open>Tools/BNF/bnf_fp_util.ML\<close>
   28.16 +ML_file \<open>Tools/BNF/bnf_fp_def_sugar_tactics.ML\<close>
   28.17 +ML_file \<open>Tools/BNF/bnf_fp_def_sugar.ML\<close>
   28.18 +ML_file \<open>Tools/BNF/bnf_fp_n2m_tactics.ML\<close>
   28.19 +ML_file \<open>Tools/BNF/bnf_fp_n2m.ML\<close>
   28.20 +ML_file \<open>Tools/BNF/bnf_fp_n2m_sugar.ML\<close>
   28.21  
   28.22  end
    29.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Jan 06 13:44:33 2019 +0100
    29.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Jan 06 15:04:34 2019 +0100
    29.3 @@ -281,10 +281,10 @@
    29.4    thus "univ f X \<in> B" using x PRES by simp
    29.5  qed
    29.6  
    29.7 -ML_file "Tools/BNF/bnf_gfp_util.ML"
    29.8 -ML_file "Tools/BNF/bnf_gfp_tactics.ML"
    29.9 -ML_file "Tools/BNF/bnf_gfp.ML"
   29.10 -ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
   29.11 -ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
   29.12 +ML_file \<open>Tools/BNF/bnf_gfp_util.ML\<close>
   29.13 +ML_file \<open>Tools/BNF/bnf_gfp_tactics.ML\<close>
   29.14 +ML_file \<open>Tools/BNF/bnf_gfp.ML\<close>
   29.15 +ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar_tactics.ML\<close>
   29.16 +ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar.ML\<close>
   29.17  
   29.18  end
    30.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Sun Jan 06 13:44:33 2019 +0100
    30.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Sun Jan 06 15:04:34 2019 +0100
    30.3 @@ -196,11 +196,11 @@
    30.4  lemma pred_fun_True_id: "NO_MATCH id p \<Longrightarrow> pred_fun (\<lambda>x. True) p f = pred_fun (\<lambda>x. True) id (p \<circ> f)"
    30.5    unfolding fun.pred_map unfolding comp_def id_def ..
    30.6  
    30.7 -ML_file "Tools/BNF/bnf_lfp_util.ML"
    30.8 -ML_file "Tools/BNF/bnf_lfp_tactics.ML"
    30.9 -ML_file "Tools/BNF/bnf_lfp.ML"
   30.10 -ML_file "Tools/BNF/bnf_lfp_compat.ML"
   30.11 -ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
   30.12 -ML_file "Tools/BNF/bnf_lfp_size.ML"
   30.13 +ML_file \<open>Tools/BNF/bnf_lfp_util.ML\<close>
   30.14 +ML_file \<open>Tools/BNF/bnf_lfp_tactics.ML\<close>
   30.15 +ML_file \<open>Tools/BNF/bnf_lfp.ML\<close>
   30.16 +ML_file \<open>Tools/BNF/bnf_lfp_compat.ML\<close>
   30.17 +ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar_more.ML\<close>
   30.18 +ML_file \<open>Tools/BNF/bnf_lfp_size.ML\<close>
   30.19  
   30.20  end
    31.1 --- a/src/HOL/Basic_BNF_LFPs.thy	Sun Jan 06 13:44:33 2019 +0100
    31.2 +++ b/src/HOL/Basic_BNF_LFPs.thy	Sun Jan 06 15:04:34 2019 +0100
    31.3 @@ -102,7 +102,7 @@
    31.4  lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))"
    31.5    by (force simp: rel_prod.simps elim: rel_prod.cases)
    31.6  
    31.7 -ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    31.8 +ML_file \<open>Tools/BNF/bnf_lfp_basic_sugar.ML\<close>
    31.9  
   31.10  declare prod.size [no_atp]
   31.11  
    32.1 --- a/src/HOL/Code_Evaluation.thy	Sun Jan 06 13:44:33 2019 +0100
    32.2 +++ b/src/HOL/Code_Evaluation.thy	Sun Jan 06 15:04:34 2019 +0100
    32.3 @@ -94,11 +94,11 @@
    32.4  | constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
    32.5  | constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
    32.6  
    32.7 -ML_file "Tools/code_evaluation.ML"
    32.8 +ML_file \<open>Tools/code_evaluation.ML\<close>
    32.9  
   32.10  code_reserved Eval Code_Evaluation
   32.11  
   32.12 -ML_file "~~/src/HOL/Tools/value_command.ML"
   32.13 +ML_file \<open>~~/src/HOL/Tools/value_command.ML\<close>
   32.14  
   32.15  
   32.16  subsection \<open>Dedicated \<open>term_of\<close> instances\<close>
   32.17 @@ -141,7 +141,7 @@
   32.18  
   32.19  subsection \<open>Generic reification\<close>
   32.20  
   32.21 -ML_file "~~/src/HOL/Tools/reification.ML"
   32.22 +ML_file \<open>~~/src/HOL/Tools/reification.ML\<close>
   32.23  
   32.24  
   32.25  subsection \<open>Diagnostic\<close>
    33.1 --- a/src/HOL/Ctr_Sugar.thy	Sun Jan 06 13:44:33 2019 +0100
    33.2 +++ b/src/HOL/Ctr_Sugar.thy	Sun Jan 06 15:04:34 2019 +0100
    33.3 @@ -27,7 +27,7 @@
    33.4  declare [[coercion_args case_abs -]]
    33.5  declare [[coercion_args case_elem - +]]
    33.6  
    33.7 -ML_file "Tools/Ctr_Sugar/case_translation.ML"
    33.8 +ML_file \<open>Tools/Ctr_Sugar/case_translation.ML\<close>
    33.9  
   33.10  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
   33.11    by (erule iffI) (erule contrapos_pn)
   33.12 @@ -37,13 +37,13 @@
   33.13    "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
   33.14    by blast+
   33.15  
   33.16 -ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
   33.17 -ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
   33.18 -ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
   33.19 -ML_file "Tools/Ctr_Sugar/ctr_sugar.ML"
   33.20 +ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_util.ML\<close>
   33.21 +ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_tactics.ML\<close>
   33.22 +ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_code.ML\<close>
   33.23 +ML_file \<open>Tools/Ctr_Sugar/ctr_sugar.ML\<close>
   33.24  
   33.25  text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close>
   33.26  
   33.27 -ML_file "Tools/coinduction.ML"
   33.28 +ML_file \<open>Tools/coinduction.ML\<close>
   33.29  
   33.30  end
    34.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Jan 06 13:44:33 2019 +0100
    34.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Jan 06 15:04:34 2019 +0100
    34.3 @@ -1635,7 +1635,7 @@
    34.4    "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
    34.5    by (simp_all add: real_div_nat_eq_floor_of_divide minus_div_mult_eq_mod [symmetric])
    34.6  
    34.7 -ML_file "approximation.ML"
    34.8 +ML_file \<open>approximation.ML\<close>
    34.9  
   34.10  method_setup approximation = \<open>
   34.11    let
   34.12 @@ -1667,7 +1667,7 @@
   34.13      "\<not> \<not> q \<longleftrightarrow> q"
   34.14    by auto
   34.15  
   34.16 -ML_file "approximation_generator.ML"
   34.17 +ML_file \<open>approximation_generator.ML\<close>
   34.18  setup "Approximation_Generator.setup"
   34.19  
   34.20  end
    35.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sun Jan 06 13:44:33 2019 +0100
    35.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Jan 06 15:04:34 2019 +0100
    35.3 @@ -2527,7 +2527,7 @@
    35.4  end
    35.5  \<close>
    35.6  
    35.7 -ML_file "cooper_tac.ML"
    35.8 +ML_file \<open>cooper_tac.ML\<close>
    35.9  
   35.10  method_setup cooper = \<open>
   35.11    Scan.lift (Args.mode "no_quantify") >>
    36.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Jan 06 13:44:33 2019 +0100
    36.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Jan 06 15:04:34 2019 +0100
    36.3 @@ -9,8 +9,8 @@
    36.4  imports Main
    36.5  begin
    36.6  
    36.7 -ML_file "langford_data.ML"
    36.8 -ML_file "ferrante_rackoff_data.ML"
    36.9 +ML_file \<open>langford_data.ML\<close>
   36.10 +ML_file \<open>ferrante_rackoff_data.ML\<close>
   36.11  
   36.12  context linorder
   36.13  begin
   36.14 @@ -424,7 +424,7 @@
   36.15  
   36.16  lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
   36.17  
   36.18 -ML_file "langford.ML"
   36.19 +ML_file \<open>langford.ML\<close>
   36.20  method_setup dlo = \<open>
   36.21    Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
   36.22  \<close> "Langford's algorithm for quantifier elimination in dense linear orders"
   36.23 @@ -746,7 +746,7 @@
   36.24  
   36.25  end
   36.26  
   36.27 -ML_file "ferrante_rackoff.ML"
   36.28 +ML_file \<open>ferrante_rackoff.ML\<close>
   36.29  
   36.30  method_setup ferrack = \<open>
   36.31    Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
    37.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Jan 06 13:44:33 2019 +0100
    37.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sun Jan 06 15:04:34 2019 +0100
    37.3 @@ -2546,7 +2546,7 @@
    37.4  end
    37.5  \<close>
    37.6  
    37.7 -ML_file "ferrack_tac.ML"
    37.8 +ML_file \<open>ferrack_tac.ML\<close>
    37.9  
   37.10  method_setup rferrack = \<open>
   37.11    Scan.lift (Args.mode "no_quantify") >>
    38.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Jan 06 13:44:33 2019 +0100
    38.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Jan 06 15:04:34 2019 +0100
    38.3 @@ -5696,7 +5696,7 @@
    38.4                           of_int_less_iff [where 'a = real, symmetric]
    38.5                           of_int_le_iff [where 'a = real, symmetric]
    38.6  
    38.7 -ML_file "mir_tac.ML"
    38.8 +ML_file \<open>mir_tac.ML\<close>
    38.9  
   38.10  method_setup mir = \<open>
   38.11    Scan.lift (Args.mode "no_quantify") >>
    39.1 --- a/src/HOL/Eisbach/Eisbach.thy	Sun Jan 06 13:44:33 2019 +0100
    39.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Sun Jan 06 15:04:34 2019 +0100
    39.3 @@ -15,10 +15,10 @@
    39.4    "uses"
    39.5  begin
    39.6  
    39.7 -ML_file "parse_tools.ML"
    39.8 -ML_file "method_closure.ML"
    39.9 -ML_file "eisbach_rule_insts.ML"
   39.10 -ML_file "match_method.ML"
   39.11 +ML_file \<open>parse_tools.ML\<close>
   39.12 +ML_file \<open>method_closure.ML\<close>
   39.13 +ML_file \<open>eisbach_rule_insts.ML\<close>
   39.14 +ML_file \<open>match_method.ML\<close>
   39.15  
   39.16  
   39.17  method solves methods m = (m; fail)
    40.1 --- a/src/HOL/Extraction.thy	Sun Jan 06 13:44:33 2019 +0100
    40.2 +++ b/src/HOL/Extraction.thy	Sun Jan 06 15:04:34 2019 +0100
    40.3 @@ -8,7 +8,7 @@
    40.4  imports Option
    40.5  begin
    40.6  
    40.7 -ML_file "Tools/rewrite_hol_proof.ML"
    40.8 +ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
    40.9  
   40.10  subsection \<open>Setup\<close>
   40.11  
    41.1 --- a/src/HOL/Fields.thy	Sun Jan 06 13:44:33 2019 +0100
    41.2 +++ b/src/HOL/Fields.thy	Sun Jan 06 15:04:34 2019 +0100
    41.3 @@ -57,8 +57,8 @@
    41.4  
    41.5  text \<open>Setup for linear arithmetic prover\<close>
    41.6  
    41.7 -ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    41.8 -ML_file "Tools/lin_arith.ML"
    41.9 +ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
   41.10 +ML_file \<open>Tools/lin_arith.ML\<close>
   41.11  setup \<open>Lin_Arith.global_setup\<close>
   41.12  declaration \<open>K Lin_Arith.setup\<close>
   41.13  
    42.1 --- a/src/HOL/Fun.thy	Sun Jan 06 13:44:33 2019 +0100
    42.2 +++ b/src/HOL/Fun.thy	Sun Jan 06 15:04:34 2019 +0100
    42.3 @@ -886,7 +886,7 @@
    42.4  
    42.5  subsubsection \<open>Functorial structure of types\<close>
    42.6  
    42.7 -ML_file "Tools/functor.ML"
    42.8 +ML_file \<open>Tools/functor.ML\<close>
    42.9  
   42.10  functor map_fun: map_fun
   42.11    by (simp_all add: fun_eq_iff)
    43.1 --- a/src/HOL/Fun_Def.thy	Sun Jan 06 13:44:33 2019 +0100
    43.2 +++ b/src/HOL/Fun_Def.thy	Sun Jan 06 15:04:34 2019 +0100
    43.3 @@ -77,25 +77,25 @@
    43.4  lemma wf_in_rel: "wf R \<Longrightarrow> wfP (in_rel R)"
    43.5    by (simp add: wfP_def)
    43.6  
    43.7 -ML_file "Tools/Function/function_core.ML"
    43.8 -ML_file "Tools/Function/mutual.ML"
    43.9 -ML_file "Tools/Function/pattern_split.ML"
   43.10 -ML_file "Tools/Function/relation.ML"
   43.11 -ML_file "Tools/Function/function_elims.ML"
   43.12 +ML_file \<open>Tools/Function/function_core.ML\<close>
   43.13 +ML_file \<open>Tools/Function/mutual.ML\<close>
   43.14 +ML_file \<open>Tools/Function/pattern_split.ML\<close>
   43.15 +ML_file \<open>Tools/Function/relation.ML\<close>
   43.16 +ML_file \<open>Tools/Function/function_elims.ML\<close>
   43.17  
   43.18  method_setup relation = \<open>
   43.19    Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
   43.20  \<close> "prove termination using a user-specified wellfounded relation"
   43.21  
   43.22 -ML_file "Tools/Function/function.ML"
   43.23 -ML_file "Tools/Function/pat_completeness.ML"
   43.24 +ML_file \<open>Tools/Function/function.ML\<close>
   43.25 +ML_file \<open>Tools/Function/pat_completeness.ML\<close>
   43.26  
   43.27  method_setup pat_completeness = \<open>
   43.28    Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
   43.29  \<close> "prove completeness of (co)datatype patterns"
   43.30  
   43.31 -ML_file "Tools/Function/fun.ML"
   43.32 -ML_file "Tools/Function/induction_schema.ML"
   43.33 +ML_file \<open>Tools/Function/fun.ML\<close>
   43.34 +ML_file \<open>Tools/Function/induction_schema.ML\<close>
   43.35  
   43.36  method_setup induction_schema = \<open>
   43.37    Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
   43.38 @@ -108,7 +108,7 @@
   43.39    where is_measure_trivial: "is_measure f"
   43.40  
   43.41  named_theorems measure_function "rules that guide the heuristic generation of measure functions"
   43.42 -ML_file "Tools/Function/measure_functions.ML"
   43.43 +ML_file \<open>Tools/Function/measure_functions.ML\<close>
   43.44  
   43.45  lemma measure_size[measure_function]: "is_measure size"
   43.46    by (rule is_measure_trivial)
   43.47 @@ -119,7 +119,7 @@
   43.48  lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   43.49    by (rule is_measure_trivial)
   43.50  
   43.51 -ML_file "Tools/Function/lexicographic_order.ML"
   43.52 +ML_file \<open>Tools/Function/lexicographic_order.ML\<close>
   43.53  
   43.54  method_setup lexicographic_order = \<open>
   43.55    Method.sections clasimp_modifiers >>
   43.56 @@ -290,10 +290,10 @@
   43.57  
   43.58  subsection \<open>Tool setup\<close>
   43.59  
   43.60 -ML_file "Tools/Function/termination.ML"
   43.61 -ML_file "Tools/Function/scnp_solve.ML"
   43.62 -ML_file "Tools/Function/scnp_reconstruct.ML"
   43.63 -ML_file "Tools/Function/fun_cases.ML"
   43.64 +ML_file \<open>Tools/Function/termination.ML\<close>
   43.65 +ML_file \<open>Tools/Function/scnp_solve.ML\<close>
   43.66 +ML_file \<open>Tools/Function/scnp_reconstruct.ML\<close>
   43.67 +ML_file \<open>Tools/Function/fun_cases.ML\<close>
   43.68  
   43.69  ML_val \<comment> \<open>setup inactive\<close>
   43.70  \<open>
    44.1 --- a/src/HOL/Fun_Def_Base.thy	Sun Jan 06 13:44:33 2019 +0100
    44.2 +++ b/src/HOL/Fun_Def_Base.thy	Sun Jan 06 15:04:34 2019 +0100
    44.3 @@ -8,15 +8,15 @@
    44.4  imports Ctr_Sugar Set Wellfounded
    44.5  begin
    44.6  
    44.7 -ML_file "Tools/Function/function_lib.ML"
    44.8 +ML_file \<open>Tools/Function/function_lib.ML\<close>
    44.9  named_theorems termination_simp "simplification rules for termination proofs"
   44.10 -ML_file "Tools/Function/function_common.ML"
   44.11 -ML_file "Tools/Function/function_context_tree.ML"
   44.12 +ML_file \<open>Tools/Function/function_common.ML\<close>
   44.13 +ML_file \<open>Tools/Function/function_context_tree.ML\<close>
   44.14  
   44.15  attribute_setup fundef_cong =
   44.16    \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close>
   44.17    "declaration of congruence rule for function definitions"
   44.18  
   44.19 -ML_file "Tools/Function/sum_tree.ML"
   44.20 +ML_file \<open>Tools/Function/sum_tree.ML\<close>
   44.21  
   44.22  end
    45.1 --- a/src/HOL/Groebner_Basis.thy	Sun Jan 06 13:44:33 2019 +0100
    45.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Jan 06 15:04:34 2019 +0100
    45.3 @@ -33,7 +33,7 @@
    45.4    by auto
    45.5  
    45.6  named_theorems algebra "pre-simplification rules for algebraic methods"
    45.7 -ML_file "Tools/groebner.ML"
    45.8 +ML_file \<open>Tools/groebner.ML\<close>
    45.9  
   45.10  method_setup algebra = \<open>
   45.11    let
    46.1 --- a/src/HOL/Groups.thy	Sun Jan 06 13:44:33 2019 +0100
    46.2 +++ b/src/HOL/Groups.thy	Sun Jan 06 15:04:34 2019 +0100
    46.3 @@ -988,7 +988,7 @@
    46.4  
    46.5  end
    46.6  
    46.7 -ML_file "Tools/group_cancel.ML"
    46.8 +ML_file \<open>Tools/group_cancel.ML\<close>
    46.9  
   46.10  simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   46.11    \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
    47.1 --- a/src/HOL/HOL.thy	Sun Jan 06 13:44:33 2019 +0100
    47.2 +++ b/src/HOL/HOL.thy	Sun Jan 06 15:04:34 2019 +0100
    47.3 @@ -12,26 +12,26 @@
    47.4    "quickcheck_params" :: thy_decl
    47.5  begin
    47.6  
    47.7 -ML_file "~~/src/Tools/misc_legacy.ML"
    47.8 -ML_file "~~/src/Tools/try.ML"
    47.9 -ML_file "~~/src/Tools/quickcheck.ML"
   47.10 -ML_file "~~/src/Tools/solve_direct.ML"
   47.11 -ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
   47.12 -ML_file "~~/src/Tools/IsaPlanner/isand.ML"
   47.13 -ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
   47.14 -ML_file "~~/src/Provers/hypsubst.ML"
   47.15 -ML_file "~~/src/Provers/splitter.ML"
   47.16 -ML_file "~~/src/Provers/classical.ML"
   47.17 -ML_file "~~/src/Provers/blast.ML"
   47.18 -ML_file "~~/src/Provers/clasimp.ML"
   47.19 -ML_file "~~/src/Tools/eqsubst.ML"
   47.20 -ML_file "~~/src/Provers/quantifier1.ML"
   47.21 -ML_file "~~/src/Tools/atomize_elim.ML"
   47.22 -ML_file "~~/src/Tools/cong_tac.ML"
   47.23 -ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
   47.24 -ML_file "~~/src/Tools/project_rule.ML"
   47.25 -ML_file "~~/src/Tools/subtyping.ML"
   47.26 -ML_file "~~/src/Tools/case_product.ML"
   47.27 +ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
   47.28 +ML_file \<open>~~/src/Tools/try.ML\<close>
   47.29 +ML_file \<open>~~/src/Tools/quickcheck.ML\<close>
   47.30 +ML_file \<open>~~/src/Tools/solve_direct.ML\<close>
   47.31 +ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
   47.32 +ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
   47.33 +ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
   47.34 +ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
   47.35 +ML_file \<open>~~/src/Provers/splitter.ML\<close>
   47.36 +ML_file \<open>~~/src/Provers/classical.ML\<close>
   47.37 +ML_file \<open>~~/src/Provers/blast.ML\<close>
   47.38 +ML_file \<open>~~/src/Provers/clasimp.ML\<close>
   47.39 +ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
   47.40 +ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
   47.41 +ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
   47.42 +ML_file \<open>~~/src/Tools/cong_tac.ML\<close>
   47.43 +ML_file \<open>~~/src/Tools/intuitionistic.ML\<close> setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
   47.44 +ML_file \<open>~~/src/Tools/project_rule.ML\<close>
   47.45 +ML_file \<open>~~/src/Tools/subtyping.ML\<close>
   47.46 +ML_file \<open>~~/src/Tools/case_product.ML\<close>
   47.47  
   47.48  
   47.49  ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
   47.50 @@ -776,7 +776,7 @@
   47.51  
   47.52  subsection \<open>Package setup\<close>
   47.53  
   47.54 -ML_file "Tools/hologic.ML"
   47.55 +ML_file \<open>Tools/hologic.ML\<close>
   47.56  
   47.57  
   47.58  subsubsection \<open>Sledgehammer setup\<close>
   47.59 @@ -1202,7 +1202,7 @@
   47.60  lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   47.61    by blast
   47.62  
   47.63 -ML_file "Tools/simpdata.ML"
   47.64 +ML_file \<open>Tools/simpdata.ML\<close>
   47.65  ML \<open>open Simpdata\<close>
   47.66  
   47.67  setup \<open>
   47.68 @@ -1484,7 +1484,7 @@
   47.69  
   47.70  text \<open>Method setup.\<close>
   47.71  
   47.72 -ML_file "~~/src/Tools/induct.ML"
   47.73 +ML_file \<open>~~/src/Tools/induct.ML\<close>
   47.74  ML \<open>
   47.75  structure Induct = Induct
   47.76  (
   47.77 @@ -1499,7 +1499,7 @@
   47.78  )
   47.79  \<close>
   47.80  
   47.81 -ML_file "~~/src/Tools/induction.ML"
   47.82 +ML_file \<open>~~/src/Tools/induction.ML\<close>
   47.83  
   47.84  declaration \<open>
   47.85    fn _ => Induct.map_simpset (fn ss => ss
   47.86 @@ -1584,12 +1584,12 @@
   47.87  
   47.88  end
   47.89  
   47.90 -ML_file "~~/src/Tools/induct_tacs.ML"
   47.91 +ML_file \<open>~~/src/Tools/induct_tacs.ML\<close>
   47.92  
   47.93  
   47.94  subsubsection \<open>Coherent logic\<close>
   47.95  
   47.96 -ML_file "~~/src/Tools/coherent.ML"
   47.97 +ML_file \<open>~~/src/Tools/coherent.ML\<close>
   47.98  ML \<open>
   47.99  structure Coherent = Coherent
  47.100  (
  47.101 @@ -1735,7 +1735,7 @@
  47.102  val trans = @{thm trans}
  47.103  \<close>
  47.104  
  47.105 -ML_file "Tools/cnf.ML"
  47.106 +ML_file \<open>Tools/cnf.ML\<close>
  47.107  
  47.108  
  47.109  section \<open>\<open>NO_MATCH\<close> simproc\<close>
    48.1 --- a/src/HOL/HOLCF/Cpodef.thy	Sun Jan 06 13:44:33 2019 +0100
    48.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Sun Jan 06 15:04:34 2019 +0100
    48.3 @@ -279,6 +279,6 @@
    48.4  
    48.5  subsection \<open>HOLCF type definition package\<close>
    48.6  
    48.7 -ML_file "Tools/cpodef.ML"
    48.8 +ML_file \<open>Tools/cpodef.ML\<close>
    48.9  
   48.10  end
    49.1 --- a/src/HOL/HOLCF/Domain.thy	Sun Jan 06 13:44:33 2019 +0100
    49.2 +++ b/src/HOL/HOLCF/Domain.thy	Sun Jan 06 15:04:34 2019 +0100
    49.3 @@ -150,7 +150,7 @@
    49.4      (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>)]
    49.5  \<close>
    49.6  
    49.7 -ML_file "Tools/domaindef.ML"
    49.8 +ML_file \<open>Tools/domaindef.ML\<close>
    49.9  
   49.10  subsection \<open>Isomorphic deflations\<close>
   49.11  
   49.12 @@ -319,9 +319,9 @@
   49.13  named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
   49.14    and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
   49.15  
   49.16 -ML_file "Tools/Domain/domain_isomorphism.ML"
   49.17 -ML_file "Tools/Domain/domain_axioms.ML"
   49.18 -ML_file "Tools/Domain/domain.ML"
   49.19 +ML_file \<open>Tools/Domain/domain_isomorphism.ML\<close>
   49.20 +ML_file \<open>Tools/Domain/domain_axioms.ML\<close>
   49.21 +ML_file \<open>Tools/Domain/domain.ML\<close>
   49.22  
   49.23  lemmas [domain_defl_simps] =
   49.24    DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
    50.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Sun Jan 06 13:44:33 2019 +0100
    50.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Sun Jan 06 15:04:34 2019 +0100
    50.3 @@ -355,10 +355,10 @@
    50.4  named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
    50.5    and domain_map_ID "theorems like foo_map$ID = ID"
    50.6  
    50.7 -ML_file "Tools/Domain/domain_take_proofs.ML"
    50.8 -ML_file "Tools/cont_consts.ML"
    50.9 -ML_file "Tools/cont_proc.ML"
   50.10 -ML_file "Tools/Domain/domain_constructors.ML"
   50.11 -ML_file "Tools/Domain/domain_induction.ML"
   50.12 +ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close>
   50.13 +ML_file \<open>Tools/cont_consts.ML\<close>
   50.14 +ML_file \<open>Tools/cont_proc.ML\<close>
   50.15 +ML_file \<open>Tools/Domain/domain_constructors.ML\<close>
   50.16 +ML_file \<open>Tools/Domain/domain_induction.ML\<close>
   50.17  
   50.18  end
    51.1 --- a/src/HOL/HOLCF/Fixrec.thy	Sun Jan 06 13:44:33 2019 +0100
    51.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Sun Jan 06 15:04:34 2019 +0100
    51.3 @@ -224,8 +224,8 @@
    51.4  
    51.5  subsection \<open>Initializing the fixrec package\<close>
    51.6  
    51.7 -ML_file "Tools/holcf_library.ML"
    51.8 -ML_file "Tools/fixrec.ML"
    51.9 +ML_file \<open>Tools/holcf_library.ML\<close>
   51.10 +ML_file \<open>Tools/fixrec.ML\<close>
   51.11  
   51.12  method_setup fixrec_simp = \<open>
   51.13    Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
    52.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Jan 06 13:44:33 2019 +0100
    52.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Jan 06 15:04:34 2019 +0100
    52.3 @@ -8,7 +8,7 @@
    52.4  imports IOA.IOA Env Impl Impl_finite
    52.5  begin
    52.6  
    52.7 -ML_file "Check.ML"
    52.8 +ML_file \<open>Check.ML\<close>
    52.9  
   52.10  primrec reduce :: "'a list => 'a list"
   52.11  where
    53.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Jan 06 13:44:33 2019 +0100
    53.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Jan 06 15:04:34 2019 +0100
    53.3 @@ -903,7 +903,7 @@
    53.4  lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c"
    53.5    by (simp only: someI_ex)
    53.6  
    53.7 -ML_file "Tools/choice_specification.ML"
    53.8 +ML_file \<open>Tools/choice_specification.ML\<close>
    53.9  
   53.10  subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close>
   53.11  
    54.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Sun Jan 06 13:44:33 2019 +0100
    54.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Sun Jan 06 15:04:34 2019 +0100
    54.3 @@ -53,7 +53,7 @@
    54.4   "_hoare"      :: "['a assn,'a com,'a assn] => bool"
    54.5                   ("{_} // _ // {_}" [0,55,0] 50)
    54.6  
    54.7 -ML_file "hoare_syntax.ML"
    54.8 +ML_file \<open>hoare_syntax.ML\<close>
    54.9  parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
   54.10  print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
   54.11  
   54.12 @@ -93,7 +93,7 @@
   54.13    by blast
   54.14  
   54.15  lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
   54.16 -ML_file "hoare_tac.ML"
   54.17 +ML_file \<open>hoare_tac.ML\<close>
   54.18  
   54.19  method_setup vcg = \<open>
   54.20    Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
    55.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Jan 06 13:44:33 2019 +0100
    55.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Jan 06 15:04:34 2019 +0100
    55.3 @@ -55,7 +55,7 @@
    55.4    "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
    55.5                   ("{_} // _ // {_}" [0,55,0] 50)
    55.6  
    55.7 -ML_file "hoare_syntax.ML"
    55.8 +ML_file \<open>hoare_syntax.ML\<close>
    55.9  parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
   55.10  print_translation
   55.11    \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
   55.12 @@ -104,7 +104,7 @@
   55.13  lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
   55.14    by blast
   55.15  
   55.16 -ML_file "hoare_tac.ML"
   55.17 +ML_file \<open>hoare_tac.ML\<close>
   55.18  
   55.19  method_setup vcg = \<open>
   55.20    Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
    56.1 --- a/src/HOL/Import/Import_Setup.thy	Sun Jan 06 13:44:33 2019 +0100
    56.2 +++ b/src/HOL/Import/Import_Setup.thy	Sun Jan 06 15:04:34 2019 +0100
    56.3 @@ -10,7 +10,7 @@
    56.4  keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
    56.5  begin
    56.6  
    56.7 -ML_file "import_data.ML"
    56.8 +ML_file \<open>import_data.ML\<close>
    56.9  
   56.10  lemma light_ex_imp_nonempty:
   56.11    "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
   56.12 @@ -26,7 +26,7 @@
   56.13    "(\<And>x. f x = g x) \<Longrightarrow> f = g"
   56.14    by auto
   56.15  
   56.16 -ML_file "import_rule.ML"
   56.17 +ML_file \<open>import_rule.ML\<close>
   56.18  
   56.19  end
   56.20  
    57.1 --- a/src/HOL/Inductive.thy	Sun Jan 06 13:44:33 2019 +0100
    57.2 +++ b/src/HOL/Inductive.thy	Sun Jan 06 15:04:34 2019 +0100
    57.3 @@ -413,7 +413,7 @@
    57.4  lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
    57.5    by auto
    57.6  
    57.7 -ML_file "Tools/inductive.ML"
    57.8 +ML_file \<open>Tools/inductive.ML\<close>
    57.9  
   57.10  lemmas [mono] =
   57.11    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   57.12 @@ -514,14 +514,14 @@
   57.13  
   57.14  text \<open>Package setup.\<close>
   57.15  
   57.16 -ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
   57.17 -ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
   57.18 -ML_file "Tools/Old_Datatype/old_datatype_data.ML"
   57.19 -ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
   57.20 -ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
   57.21 -ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
   57.22 -ML_file "Tools/Old_Datatype/old_primrec.ML"
   57.23 -ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
   57.24 +ML_file \<open>Tools/Old_Datatype/old_datatype_aux.ML\<close>
   57.25 +ML_file \<open>Tools/Old_Datatype/old_datatype_prop.ML\<close>
   57.26 +ML_file \<open>Tools/Old_Datatype/old_datatype_data.ML\<close>
   57.27 +ML_file \<open>Tools/Old_Datatype/old_rep_datatype.ML\<close>
   57.28 +ML_file \<open>Tools/Old_Datatype/old_datatype_codegen.ML\<close>
   57.29 +ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_util.ML\<close>
   57.30 +ML_file \<open>Tools/Old_Datatype/old_primrec.ML\<close>
   57.31 +ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar.ML\<close>
   57.32  
   57.33  text \<open>Lambda-abstractions with pattern matching:\<close>
   57.34  syntax (ASCII)
    58.1 --- a/src/HOL/Int.thy	Sun Jan 06 13:44:33 2019 +0100
    58.2 +++ b/src/HOL/Int.thy	Sun Jan 06 15:04:34 2019 +0100
    58.3 @@ -1081,7 +1081,7 @@
    58.4  lemmas of_int_simps =
    58.5    of_int_0 of_int_1 of_int_add of_int_mult
    58.6  
    58.7 -ML_file "Tools/int_arith.ML"
    58.8 +ML_file \<open>Tools/int_arith.ML\<close>
    58.9  declaration \<open>K Int_Arith.setup\<close>
   58.10  
   58.11  simproc_setup fast_arith
    59.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Sun Jan 06 13:44:33 2019 +0100
    59.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Sun Jan 06 15:04:34 2019 +0100
    59.3 @@ -401,7 +401,7 @@
    59.4  
    59.5  lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
    59.6  
    59.7 -ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
    59.8 +ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
    59.9  
   59.10  method_setup hoare =
   59.11    \<open>Scan.succeed (fn ctxt =>
    60.1 --- a/src/HOL/Lattices.thy	Sun Jan 06 13:44:33 2019 +0100
    60.2 +++ b/src/HOL/Lattices.thy	Sun Jan 06 15:04:34 2019 +0100
    60.3 @@ -693,7 +693,7 @@
    60.4  
    60.5  end
    60.6  
    60.7 -ML_file "Tools/boolean_algebra_cancel.ML"
    60.8 +ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
    60.9  
   60.10  simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
   60.11    \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
    61.1 --- a/src/HOL/Library/Adhoc_Overloading.thy	Sun Jan 06 13:44:33 2019 +0100
    61.2 +++ b/src/HOL/Library/Adhoc_Overloading.thy	Sun Jan 06 15:04:34 2019 +0100
    61.3 @@ -10,6 +10,6 @@
    61.4    keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl
    61.5  begin
    61.6  
    61.7 -ML_file "adhoc_overloading.ML"
    61.8 +ML_file \<open>adhoc_overloading.ML\<close>
    61.9  
   61.10  end
    62.1 --- a/src/HOL/Library/BNF_Axiomatization.thy	Sun Jan 06 13:44:33 2019 +0100
    62.2 +++ b/src/HOL/Library/BNF_Axiomatization.thy	Sun Jan 06 15:04:34 2019 +0100
    62.3 @@ -13,6 +13,6 @@
    62.4    "bnf_axiomatization" :: thy_decl
    62.5  begin
    62.6  
    62.7 -ML_file "../Tools/BNF/bnf_axiomatization.ML"
    62.8 +ML_file \<open>../Tools/BNF/bnf_axiomatization.ML\<close>
    62.9  
   62.10  end
    63.1 --- a/src/HOL/Library/BNF_Corec.thy	Sun Jan 06 13:44:33 2019 +0100
    63.2 +++ b/src/HOL/Library/BNF_Corec.thy	Sun Jan 06 15:04:34 2019 +0100
    63.3 @@ -201,12 +201,12 @@
    63.4  
    63.5  named_theorems friend_of_corec_simps
    63.6  
    63.7 -ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML"
    63.8 -ML_file "../Tools/BNF/bnf_gfp_grec.ML"
    63.9 -ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML"
   63.10 -ML_file "../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
   63.11 -ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
   63.12 -ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
   63.13 +ML_file \<open>../Tools/BNF/bnf_gfp_grec_tactics.ML\<close>
   63.14 +ML_file \<open>../Tools/BNF/bnf_gfp_grec.ML\<close>
   63.15 +ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_util.ML\<close>
   63.16 +ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML\<close>
   63.17 +ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar.ML\<close>
   63.18 +ML_file \<open>../Tools/BNF/bnf_gfp_grec_unique_sugar.ML\<close>
   63.19  
   63.20  method_setup transfer_prover_eq = \<open>
   63.21    Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
    64.1 --- a/src/HOL/Library/Cancellation.thy	Sun Jan 06 13:44:33 2019 +0100
    64.2 +++ b/src/HOL/Library/Cancellation.thy	Sun Jan 06 15:04:34 2019 +0100
    64.3 @@ -76,9 +76,9 @@
    64.4  
    64.5  subsection \<open>Simproc Set-Up\<close>
    64.6  
    64.7 -ML_file "Cancellation/cancel.ML"
    64.8 -ML_file "Cancellation/cancel_data.ML"
    64.9 -ML_file "Cancellation/cancel_simprocs.ML"
   64.10 +ML_file \<open>Cancellation/cancel.ML\<close>
   64.11 +ML_file \<open>Cancellation/cancel_data.ML\<close>
   64.12 +ML_file \<open>Cancellation/cancel_simprocs.ML\<close>
   64.13  
   64.14  end
   64.15  
    65.1 --- a/src/HOL/Library/Case_Converter.thy	Sun Jan 06 13:44:33 2019 +0100
    65.2 +++ b/src/HOL/Library/Case_Converter.thy	Sun Jan 06 15:04:34 2019 +0100
    65.3 @@ -18,6 +18,6 @@
    65.4    "missing_pattern_match = Code.abort"
    65.5    unfolding missing_pattern_match_def Code.abort_def ..
    65.6  
    65.7 -ML_file "case_converter.ML"
    65.8 +ML_file \<open>case_converter.ML\<close>
    65.9  
   65.10  end
    66.1 --- a/src/HOL/Library/Code_Lazy.thy	Sun Jan 06 13:44:33 2019 +0100
    66.2 +++ b/src/HOL/Library/Code_Lazy.thy	Sun Jan 06 15:04:34 2019 +0100
    66.3 @@ -227,7 +227,7 @@
    66.4  
    66.5  subsection \<open>Implementation\<close>
    66.6  
    66.7 -ML_file "code_lazy.ML"
    66.8 +ML_file \<open>code_lazy.ML\<close>
    66.9  
   66.10  setup \<open>
   66.11    Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
    67.1 --- a/src/HOL/Library/Code_Prolog.thy	Sun Jan 06 13:44:33 2019 +0100
    67.2 +++ b/src/HOL/Library/Code_Prolog.thy	Sun Jan 06 15:04:34 2019 +0100
    67.3 @@ -9,7 +9,7 @@
    67.4  keywords "values_prolog" :: diag
    67.5  begin
    67.6  
    67.7 -ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
    67.8 +ML_file \<open>~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML\<close>
    67.9  
   67.10  section \<open>Setup for Numerals\<close>
   67.11  
    68.1 --- a/src/HOL/Library/Code_Test.thy	Sun Jan 06 13:44:33 2019 +0100
    68.2 +++ b/src/HOL/Library/Code_Test.thy	Sun Jan 06 15:04:34 2019 +0100
    68.3 @@ -142,6 +142,6 @@
    68.4  
    68.5  subsection \<open>Test engine and drivers\<close>
    68.6  
    68.7 -ML_file "code_test.ML"
    68.8 +ML_file \<open>code_test.ML\<close>
    68.9  
   68.10  end
    69.1 --- a/src/HOL/Library/Conditional_Parametricity.thy	Sun Jan 06 13:44:33 2019 +0100
    69.2 +++ b/src/HOL/Library/Conditional_Parametricity.thy	Sun Jan 06 15:04:34 2019 +0100
    69.3 @@ -43,6 +43,6 @@
    69.4  
    69.5  end
    69.6  
    69.7 -ML_file "conditional_parametricity.ML"
    69.8 +ML_file \<open>conditional_parametricity.ML\<close>
    69.9  
   69.10  end
    70.1 --- a/src/HOL/Library/Countable.thy	Sun Jan 06 13:44:33 2019 +0100
    70.2 +++ b/src/HOL/Library/Countable.thy	Sun Jan 06 15:04:34 2019 +0100
    70.3 @@ -200,7 +200,7 @@
    70.4  
    70.5  subsection \<open>Automatically proving countability of datatypes\<close>
    70.6  
    70.7 -ML_file "../Tools/BNF/bnf_lfp_countable.ML"
    70.8 +ML_file \<open>../Tools/BNF/bnf_lfp_countable.ML\<close>
    70.9  
   70.10  ML \<open>
   70.11  fun countable_datatype_tac ctxt st =
    71.1 --- a/src/HOL/Library/Datatype_Records.thy	Sun Jan 06 13:44:33 2019 +0100
    71.2 +++ b/src/HOL/Library/Datatype_Records.thy	Sun Jan 06 15:04:34 2019 +0100
    71.3 @@ -82,7 +82,7 @@
    71.4  
    71.5  named_theorems datatype_record_update
    71.6  
    71.7 -ML_file "datatype_records.ML"
    71.8 +ML_file \<open>datatype_records.ML\<close>
    71.9  setup \<open>Datatype_Records.setup\<close>
   71.10  
   71.11  end
   71.12 \ No newline at end of file
    72.1 --- a/src/HOL/Library/Multiset.thy	Sun Jan 06 13:44:33 2019 +0100
    72.2 +++ b/src/HOL/Library/Multiset.thy	Sun Jan 06 15:04:34 2019 +0100
    72.3 @@ -969,7 +969,7 @@
    72.4    unfolding subset_mset_def repeat_mset_iterate_add
    72.5    by (simp add: iterate_add_eq_add_iff2 mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add])
    72.6  
    72.7 -ML_file "multiset_simprocs.ML"
    72.8 +ML_file \<open>multiset_simprocs.ML\<close>
    72.9  
   72.10  lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close>
   72.11    by simp
    73.1 --- a/src/HOL/Library/Old_Datatype.thy	Sun Jan 06 13:44:33 2019 +0100
    73.2 +++ b/src/HOL/Library/Old_Datatype.thy	Sun Jan 06 15:04:34 2019 +0100
    73.3 @@ -508,6 +508,6 @@
    73.4  hide_type (open) node item
    73.5  hide_const (open) Push Node Atom Leaf Numb Lim Split Case
    73.6  
    73.7 -ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
    73.8 +ML_file \<open>~~/src/HOL/Tools/Old_Datatype/old_datatype.ML\<close>
    73.9  
   73.10  end
    74.1 --- a/src/HOL/Library/Old_Recdef.thy	Sun Jan 06 13:44:33 2019 +0100
    74.2 +++ b/src/HOL/Library/Old_Recdef.thy	Sun Jan 06 15:04:34 2019 +0100
    74.3 @@ -57,7 +57,7 @@
    74.4  lemma tfl_exE: "\<exists>x. P x \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q \<Longrightarrow> Q"
    74.5    by blast
    74.6  
    74.7 -ML_file "old_recdef.ML"
    74.8 +ML_file \<open>old_recdef.ML\<close>
    74.9  
   74.10  
   74.11  subsection \<open>Rule setup\<close>
    75.1 --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Jan 06 13:44:33 2019 +0100
    75.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Jan 06 15:04:34 2019 +0100
    75.3 @@ -8,6 +8,6 @@
    75.4    imports Predicate_Compile_Alternative_Defs
    75.5  begin
    75.6  
    75.7 -ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
    75.8 +ML_file \<open>../Tools/Predicate_Compile/predicate_compile_quickcheck.ML\<close>
    75.9  
   75.10  end
    76.1 --- a/src/HOL/Library/Realizers.thy	Sun Jan 06 13:44:33 2019 +0100
    76.2 +++ b/src/HOL/Library/Realizers.thy	Sun Jan 06 15:04:34 2019 +0100
    76.3 @@ -8,7 +8,7 @@
    76.4  imports Main
    76.5  begin
    76.6  
    76.7 -ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
    76.8 -ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
    76.9 +ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close>
   76.10 +ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close>
   76.11  
   76.12  end
    77.1 --- a/src/HOL/Library/Reflection.thy	Sun Jan 06 13:44:33 2019 +0100
    77.2 +++ b/src/HOL/Library/Reflection.thy	Sun Jan 06 15:04:34 2019 +0100
    77.3 @@ -8,7 +8,7 @@
    77.4  imports Main
    77.5  begin
    77.6  
    77.7 -ML_file "~~/src/HOL/Tools/reflection.ML"
    77.8 +ML_file \<open>~~/src/HOL/Tools/reflection.ML\<close>
    77.9  
   77.10  method_setup reify = \<open>
   77.11    Attrib.thms --
    78.1 --- a/src/HOL/Library/Refute.thy	Sun Jan 06 13:44:33 2019 +0100
    78.2 +++ b/src/HOL/Library/Refute.thy	Sun Jan 06 15:04:34 2019 +0100
    78.3 @@ -14,7 +14,7 @@
    78.4    "refute_params" :: thy_decl
    78.5  begin
    78.6  
    78.7 -ML_file "refute.ML"
    78.8 +ML_file \<open>refute.ML\<close>
    78.9  
   78.10  refute_params
   78.11   [itself = 1,
    79.1 --- a/src/HOL/Library/Rewrite.thy	Sun Jan 06 13:44:33 2019 +0100
    79.2 +++ b/src/HOL/Library/Rewrite.thy	Sun Jan 06 15:04:34 2019 +0100
    79.3 @@ -30,7 +30,7 @@
    79.4     apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    79.5    done
    79.6  
    79.7 -ML_file "cconv.ML"
    79.8 -ML_file "rewrite.ML"
    79.9 +ML_file \<open>cconv.ML\<close>
   79.10 +ML_file \<open>rewrite.ML\<close>
   79.11  
   79.12  end
    80.1 --- a/src/HOL/Library/Simps_Case_Conv.thy	Sun Jan 06 13:44:33 2019 +0100
    80.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Sun Jan 06 15:04:34 2019 +0100
    80.3 @@ -8,6 +8,6 @@
    80.4    abbrevs "simps_of_case" "case_of_simps" = ""
    80.5  begin
    80.6  
    80.7 -ML_file "simps_case_conv.ML"
    80.8 +ML_file \<open>simps_case_conv.ML\<close>
    80.9  
   80.10  end
    81.1 --- a/src/HOL/Library/Sum_of_Squares.thy	Sun Jan 06 13:44:33 2019 +0100
    81.2 +++ b/src/HOL/Library/Sum_of_Squares.thy	Sun Jan 06 15:04:34 2019 +0100
    81.3 @@ -10,9 +10,9 @@
    81.4  imports Complex_Main
    81.5  begin
    81.6  
    81.7 -ML_file "positivstellensatz.ML"
    81.8 -ML_file "Sum_of_Squares/sum_of_squares.ML"
    81.9 -ML_file "Sum_of_Squares/positivstellensatz_tools.ML"
   81.10 -ML_file "Sum_of_Squares/sos_wrapper.ML"
   81.11 +ML_file \<open>positivstellensatz.ML\<close>
   81.12 +ML_file \<open>Sum_of_Squares/sum_of_squares.ML\<close>
   81.13 +ML_file \<open>Sum_of_Squares/positivstellensatz_tools.ML\<close>
   81.14 +ML_file \<open>Sum_of_Squares/sos_wrapper.ML\<close>
   81.15  
   81.16  end
    82.1 --- a/src/HOL/Lifting.thy	Sun Jan 06 13:44:33 2019 +0100
    82.2 +++ b/src/HOL/Lifting.thy	Sun Jan 06 15:04:34 2019 +0100
    82.3 @@ -552,22 +552,22 @@
    82.4  
    82.5  subsection \<open>ML setup\<close>
    82.6  
    82.7 -ML_file "Tools/Lifting/lifting_util.ML"
    82.8 +ML_file \<open>Tools/Lifting/lifting_util.ML\<close>
    82.9  
   82.10  named_theorems relator_eq_onp
   82.11    "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
   82.12 -ML_file "Tools/Lifting/lifting_info.ML"
   82.13 +ML_file \<open>Tools/Lifting/lifting_info.ML\<close>
   82.14  
   82.15  (* setup for the function type *)
   82.16  declare fun_quotient[quot_map]
   82.17  declare fun_mono[relator_mono]
   82.18  lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
   82.19  
   82.20 -ML_file "Tools/Lifting/lifting_bnf.ML"
   82.21 -ML_file "Tools/Lifting/lifting_term.ML"
   82.22 -ML_file "Tools/Lifting/lifting_def.ML"
   82.23 -ML_file "Tools/Lifting/lifting_setup.ML"
   82.24 -ML_file "Tools/Lifting/lifting_def_code_dt.ML"
   82.25 +ML_file \<open>Tools/Lifting/lifting_bnf.ML\<close>
   82.26 +ML_file \<open>Tools/Lifting/lifting_term.ML\<close>
   82.27 +ML_file \<open>Tools/Lifting/lifting_def.ML\<close>
   82.28 +ML_file \<open>Tools/Lifting/lifting_setup.ML\<close>
   82.29 +ML_file \<open>Tools/Lifting/lifting_def_code_dt.ML\<close>
   82.30  
   82.31  lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
   82.32  by(cases xy) simp
    83.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Sun Jan 06 13:44:33 2019 +0100
    83.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Sun Jan 06 15:04:34 2019 +0100
    83.3 @@ -8,7 +8,7 @@
    83.4  imports Complex_Main "HOL-Library.Lattice_Algebras"
    83.5  begin
    83.6  
    83.7 -ML_file "~~/src/Tools/float.ML"
    83.8 +ML_file \<open>~~/src/Tools/float.ML\<close>
    83.9  
   83.10  (*FIXME surely floor should be used? This file is full of redundant material.*)
   83.11  
   83.12 @@ -235,6 +235,6 @@
   83.13  lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
   83.14    nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
   83.15  
   83.16 -ML_file "float_arith.ML"
   83.17 +ML_file \<open>float_arith.ML\<close>
   83.18  
   83.19  end
    84.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Sun Jan 06 13:44:33 2019 +0100
    84.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Sun Jan 06 15:04:34 2019 +0100
    84.3 @@ -7,13 +7,13 @@
    84.4  theory Compute_Oracle imports HOL.HOL
    84.5  begin
    84.6  
    84.7 -ML_file "am.ML"
    84.8 -ML_file "am_compiler.ML"
    84.9 -ML_file "am_interpreter.ML"
   84.10 -ML_file "am_ghc.ML"
   84.11 -ML_file "am_sml.ML"
   84.12 -ML_file "report.ML"
   84.13 -ML_file "compute.ML"
   84.14 -ML_file "linker.ML"
   84.15 +ML_file \<open>am.ML\<close>
   84.16 +ML_file \<open>am_compiler.ML\<close>
   84.17 +ML_file \<open>am_interpreter.ML\<close>
   84.18 +ML_file \<open>am_ghc.ML\<close>
   84.19 +ML_file \<open>am_sml.ML\<close>
   84.20 +ML_file \<open>report.ML\<close>
   84.21 +ML_file \<open>compute.ML\<close>
   84.22 +ML_file \<open>linker.ML\<close>
   84.23  
   84.24  end
    85.1 --- a/src/HOL/Matrix_LP/Cplex.thy	Sun Jan 06 13:44:33 2019 +0100
    85.2 +++ b/src/HOL/Matrix_LP/Cplex.thy	Sun Jan 06 15:04:34 2019 +0100
    85.3 @@ -6,10 +6,10 @@
    85.4  imports SparseMatrix LP ComputeFloat ComputeNumeral
    85.5  begin
    85.6  
    85.7 -ML_file "Cplex_tools.ML"
    85.8 -ML_file "CplexMatrixConverter.ML"
    85.9 -ML_file "FloatSparseMatrixBuilder.ML"
   85.10 -ML_file "fspmlp.ML"
   85.11 +ML_file \<open>Cplex_tools.ML\<close>
   85.12 +ML_file \<open>CplexMatrixConverter.ML\<close>
   85.13 +ML_file \<open>FloatSparseMatrixBuilder.ML\<close>
   85.14 +ML_file \<open>fspmlp.ML\<close>
   85.15  
   85.16  lemma spm_mult_le_dual_prts: 
   85.17    assumes
   85.18 @@ -64,7 +64,7 @@
   85.19    (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
   85.20    by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
   85.21  
   85.22 -ML_file "matrixlp.ML"
   85.23 +ML_file \<open>matrixlp.ML\<close>
   85.24  
   85.25  end
   85.26  
    86.1 --- a/src/HOL/Meson.thy	Sun Jan 06 13:44:33 2019 +0100
    86.2 +++ b/src/HOL/Meson.thy	Sun Jan 06 15:04:34 2019 +0100
    86.3 @@ -195,9 +195,9 @@
    86.4  
    86.5  subsection \<open>Meson package\<close>
    86.6  
    86.7 -ML_file "Tools/Meson/meson.ML"
    86.8 -ML_file "Tools/Meson/meson_clausify.ML"
    86.9 -ML_file "Tools/Meson/meson_tactic.ML"
   86.10 +ML_file \<open>Tools/Meson/meson.ML\<close>
   86.11 +ML_file \<open>Tools/Meson/meson_clausify.ML\<close>
   86.12 +ML_file \<open>Tools/Meson/meson_tactic.ML\<close>
   86.13  
   86.14  hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
   86.15  hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
    87.1 --- a/src/HOL/Metis.thy	Sun Jan 06 13:44:33 2019 +0100
    87.2 +++ b/src/HOL/Metis.thy	Sun Jan 06 15:04:34 2019 +0100
    87.3 @@ -10,7 +10,7 @@
    87.4  imports ATP
    87.5  begin
    87.6  
    87.7 -ML_file "~~/src/Tools/Metis/metis.ML"
    87.8 +ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
    87.9  
   87.10  
   87.11  subsection \<open>Literal selection and lambda-lifting helpers\<close>
   87.12 @@ -38,9 +38,9 @@
   87.13  
   87.14  subsection \<open>Metis package\<close>
   87.15  
   87.16 -ML_file "Tools/Metis/metis_generate.ML"
   87.17 -ML_file "Tools/Metis/metis_reconstruct.ML"
   87.18 -ML_file "Tools/Metis/metis_tactic.ML"
   87.19 +ML_file \<open>Tools/Metis/metis_generate.ML\<close>
   87.20 +ML_file \<open>Tools/Metis/metis_reconstruct.ML\<close>
   87.21 +ML_file \<open>Tools/Metis/metis_tactic.ML\<close>
   87.22  
   87.23  hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
   87.24  hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
    88.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Sun Jan 06 13:44:33 2019 +0100
    88.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Sun Jan 06 15:04:34 2019 +0100
    88.3 @@ -6,8 +6,8 @@
    88.4  imports Main
    88.5  begin
    88.6  
    88.7 -ML_file "Tools/mirabelle.ML"
    88.8 -ML_file "../TPTP/sledgehammer_tactics.ML"
    88.9 +ML_file \<open>Tools/mirabelle.ML\<close>
   88.10 +ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close>
   88.11  
   88.12  ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close>
   88.13  
    89.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Sun Jan 06 13:44:33 2019 +0100
    89.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sun Jan 06 15:04:34 2019 +0100
    89.3 @@ -8,13 +8,13 @@
    89.4  imports Main Mirabelle
    89.5  begin
    89.6  
    89.7 -ML_file "Tools/mirabelle_arith.ML"
    89.8 -ML_file "Tools/mirabelle_metis.ML"
    89.9 -ML_file "Tools/mirabelle_quickcheck.ML"
   89.10 -ML_file "Tools/mirabelle_refute.ML"
   89.11 -ML_file "Tools/mirabelle_sledgehammer.ML"
   89.12 -ML_file "Tools/mirabelle_sledgehammer_filter.ML"
   89.13 -ML_file "Tools/mirabelle_try0.ML"
   89.14 +ML_file \<open>Tools/mirabelle_arith.ML\<close>
   89.15 +ML_file \<open>Tools/mirabelle_metis.ML\<close>
   89.16 +ML_file \<open>Tools/mirabelle_quickcheck.ML\<close>
   89.17 +ML_file \<open>Tools/mirabelle_refute.ML\<close>
   89.18 +ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close>
   89.19 +ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close>
   89.20 +ML_file \<open>Tools/mirabelle_try0.ML\<close>
   89.21  
   89.22  text \<open>
   89.23    Only perform type-checking of the actions,
    90.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sun Jan 06 13:44:33 2019 +0100
    90.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sun Jan 06 15:04:34 2019 +0100
    90.3 @@ -11,8 +11,8 @@
    90.4    "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
    90.5  begin
    90.6  
    90.7 -ML_file "mutabelle.ML"
    90.8 -ML_file "mutabelle_extra.ML"
    90.9 +ML_file \<open>mutabelle.ML\<close>
   90.10 +ML_file \<open>mutabelle_extra.ML\<close>
   90.11  
   90.12  
   90.13  section \<open>configuration\<close>
    91.1 --- a/src/HOL/Nat.thy	Sun Jan 06 13:44:33 2019 +0100
    91.2 +++ b/src/HOL/Nat.thy	Sun Jan 06 15:04:34 2019 +0100
    91.3 @@ -1930,7 +1930,7 @@
    91.4    shows "u = s"
    91.5    using assms(2,1) by (rule trans)
    91.6  
    91.7 -ML_file "Tools/nat_arith.ML"
    91.8 +ML_file \<open>Tools/nat_arith.ML\<close>
    91.9  
   91.10  simproc_setup nateq_cancel_sums
   91.11    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
    92.1 --- a/src/HOL/Nitpick.thy	Sun Jan 06 13:44:33 2019 +0100
    92.2 +++ b/src/HOL/Nitpick.thy	Sun Jan 06 15:04:34 2019 +0100
    92.3 @@ -201,21 +201,21 @@
    92.4  definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    92.5    "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x else THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y"
    92.6  
    92.7 -ML_file "Tools/Nitpick/kodkod.ML"
    92.8 -ML_file "Tools/Nitpick/kodkod_sat.ML"
    92.9 -ML_file "Tools/Nitpick/nitpick_util.ML"
   92.10 -ML_file "Tools/Nitpick/nitpick_hol.ML"
   92.11 -ML_file "Tools/Nitpick/nitpick_mono.ML"
   92.12 -ML_file "Tools/Nitpick/nitpick_preproc.ML"
   92.13 -ML_file "Tools/Nitpick/nitpick_scope.ML"
   92.14 -ML_file "Tools/Nitpick/nitpick_peephole.ML"
   92.15 -ML_file "Tools/Nitpick/nitpick_rep.ML"
   92.16 -ML_file "Tools/Nitpick/nitpick_nut.ML"
   92.17 -ML_file "Tools/Nitpick/nitpick_kodkod.ML"
   92.18 -ML_file "Tools/Nitpick/nitpick_model.ML"
   92.19 -ML_file "Tools/Nitpick/nitpick.ML"
   92.20 -ML_file "Tools/Nitpick/nitpick_commands.ML"
   92.21 -ML_file "Tools/Nitpick/nitpick_tests.ML"
   92.22 +ML_file \<open>Tools/Nitpick/kodkod.ML\<close>
   92.23 +ML_file \<open>Tools/Nitpick/kodkod_sat.ML\<close>
   92.24 +ML_file \<open>Tools/Nitpick/nitpick_util.ML\<close>
   92.25 +ML_file \<open>Tools/Nitpick/nitpick_hol.ML\<close>
   92.26 +ML_file \<open>Tools/Nitpick/nitpick_mono.ML\<close>
   92.27 +ML_file \<open>Tools/Nitpick/nitpick_preproc.ML\<close>
   92.28 +ML_file \<open>Tools/Nitpick/nitpick_scope.ML\<close>
   92.29 +ML_file \<open>Tools/Nitpick/nitpick_peephole.ML\<close>
   92.30 +ML_file \<open>Tools/Nitpick/nitpick_rep.ML\<close>
   92.31 +ML_file \<open>Tools/Nitpick/nitpick_nut.ML\<close>
   92.32 +ML_file \<open>Tools/Nitpick/nitpick_kodkod.ML\<close>
   92.33 +ML_file \<open>Tools/Nitpick/nitpick_model.ML\<close>
   92.34 +ML_file \<open>Tools/Nitpick/nitpick.ML\<close>
   92.35 +ML_file \<open>Tools/Nitpick/nitpick_commands.ML\<close>
   92.36 +ML_file \<open>Tools/Nitpick/nitpick_tests.ML\<close>
   92.37  
   92.38  setup \<open>
   92.39    Nitpick_HOL.register_ersatz_global
    93.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sun Jan 06 13:44:33 2019 +0100
    93.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sun Jan 06 15:04:34 2019 +0100
    93.3 @@ -11,7 +11,7 @@
    93.4  imports Main
    93.5  begin
    93.6  
    93.7 -ML_file "minipick.ML"
    93.8 +ML_file \<open>minipick.ML\<close>
    93.9  
   93.10  nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
   93.11    total_consts = smart]
    94.1 --- a/src/HOL/Nominal/Nominal.thy	Sun Jan 06 13:44:33 2019 +0100
    94.2 +++ b/src/HOL/Nominal/Nominal.thy	Sun Jan 06 15:04:34 2019 +0100
    94.3 @@ -3561,7 +3561,7 @@
    94.4  
    94.5  (*******************************************************)
    94.6  (* Setup of the theorem attributes eqvt and eqvt_force *)
    94.7 -ML_file "nominal_thmdecls.ML"
    94.8 +ML_file \<open>nominal_thmdecls.ML\<close>
    94.9  setup "NominalThmDecls.setup"
   94.10  
   94.11  lemmas [eqvt] = 
   94.12 @@ -3597,11 +3597,11 @@
   94.13  (***************************************)
   94.14  (* setup for the individial atom-kinds *)
   94.15  (* and nominal datatypes               *)
   94.16 -ML_file "nominal_atoms.ML"
   94.17 +ML_file \<open>nominal_atoms.ML\<close>
   94.18  
   94.19  (************************************************************)
   94.20  (* various tactics for analysing permutations, supports etc *)
   94.21 -ML_file "nominal_permeq.ML"
   94.22 +ML_file \<open>nominal_permeq.ML\<close>
   94.23  
   94.24  method_setup perm_simp =
   94.25    \<open>NominalPermeq.perm_simp_meth\<close>
   94.26 @@ -3645,7 +3645,7 @@
   94.27  
   94.28  (*****************************************************************)
   94.29  (* tactics for generating fresh names and simplifying fresh_funs *)
   94.30 -ML_file "nominal_fresh_fun.ML"
   94.31 +ML_file \<open>nominal_fresh_fun.ML\<close>
   94.32  
   94.33  method_setup generate_fresh = \<open>
   94.34    Args.type_name {proper = true, strict = true} >>
   94.35 @@ -3663,20 +3663,20 @@
   94.36  lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
   94.37    using assms ..
   94.38  
   94.39 -ML_file "nominal_datatype.ML"
   94.40 +ML_file \<open>nominal_datatype.ML\<close>
   94.41  
   94.42  (******************************************************)
   94.43  (* primitive recursive functions on nominal datatypes *)
   94.44 -ML_file "nominal_primrec.ML"
   94.45 +ML_file \<open>nominal_primrec.ML\<close>
   94.46  
   94.47  (****************************************************)
   94.48  (* inductive definition involving nominal datatypes *)
   94.49 -ML_file "nominal_inductive.ML"
   94.50 -ML_file "nominal_inductive2.ML"
   94.51 +ML_file \<open>nominal_inductive.ML\<close>
   94.52 +ML_file \<open>nominal_inductive2.ML\<close>
   94.53  
   94.54  (*****************************************)
   94.55  (* setup for induction principles method *)
   94.56 -ML_file "nominal_induct.ML"
   94.57 +ML_file \<open>nominal_induct.ML\<close>
   94.58  method_setup nominal_induct =
   94.59    \<open>NominalInduct.nominal_induct_method\<close>
   94.60    \<open>nominal induction\<close>
    95.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Jan 06 13:44:33 2019 +0100
    95.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Jan 06 15:04:34 2019 +0100
    95.3 @@ -99,7 +99,7 @@
    95.4    where "star_of x \<equiv> star_n (\<lambda>n. x)"
    95.5  
    95.6  text \<open>Initialize transfer tactic.\<close>
    95.7 -ML_file "transfer_principle.ML"
    95.8 +ML_file \<open>transfer_principle.ML\<close>
    95.9  
   95.10  method_setup transfer =
   95.11    \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))\<close>
    96.1 --- a/src/HOL/Num.thy	Sun Jan 06 13:44:33 2019 +0100
    96.2 +++ b/src/HOL/Num.thy	Sun Jan 06 15:04:34 2019 +0100
    96.3 @@ -292,7 +292,7 @@
    96.4  syntax
    96.5    "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
    96.6  
    96.7 -ML_file "Tools/numeral.ML"
    96.8 +ML_file \<open>Tools/numeral.ML\<close>
    96.9  
   96.10  parse_translation \<open>
   96.11    let
    97.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Jan 06 13:44:33 2019 +0100
    97.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sun Jan 06 15:04:34 2019 +0100
    97.3 @@ -6,11 +6,11 @@
    97.4  imports Divides
    97.5  begin
    97.6  
    97.7 -ML_file "~~/src/Provers/Arith/assoc_fold.ML"
    97.8 -ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
    97.9 -ML_file "~~/src/Provers/Arith/combine_numerals.ML"
   97.10 -ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
   97.11 -ML_file "~~/src/Provers/Arith/extract_common_term.ML"
   97.12 +ML_file \<open>~~/src/Provers/Arith/assoc_fold.ML\<close>
   97.13 +ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
   97.14 +ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
   97.15 +ML_file \<open>~~/src/Provers/Arith/cancel_numeral_factor.ML\<close>
   97.16 +ML_file \<open>~~/src/Provers/Arith/extract_common_term.ML\<close>
   97.17  
   97.18  lemmas semiring_norm =
   97.19    Let_def arith_simps diff_nat_numeral rel_simps
   97.20 @@ -103,7 +103,7 @@
   97.21    fixes x:: "'a::comm_ring_1" shows  "numeral w * -x = x * - numeral w"
   97.22    by (simp add: mult.commute)
   97.23  
   97.24 -ML_file "Tools/numeral_simprocs.ML"
   97.25 +ML_file \<open>Tools/numeral_simprocs.ML\<close>
   97.26  
   97.27  simproc_setup semiring_assoc_fold
   97.28    ("(a::'a::comm_semiring_1_cancel) * b") =
   97.29 @@ -213,7 +213,7 @@
   97.30    |"(l::'a::field) / (m * n)") =
   97.31    \<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>
   97.32  
   97.33 -ML_file "Tools/nat_numeral_simprocs.ML"
   97.34 +ML_file \<open>Tools/nat_numeral_simprocs.ML\<close>
   97.35  
   97.36  simproc_setup nat_combine_numerals
   97.37    ("(i::nat) + j" | "Suc (i + j)") =
    98.1 --- a/src/HOL/Nunchaku.thy	Sun Jan 06 13:44:33 2019 +0100
    98.2 +++ b/src/HOL/Nunchaku.thy	Sun Jan 06 15:04:34 2019 +0100
    98.3 @@ -29,16 +29,16 @@
    98.4  definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
    98.5    "rmember A x \<longleftrightarrow> x \<in> A"
    98.6  
    98.7 -ML_file "Tools/Nunchaku/nunchaku_util.ML"
    98.8 -ML_file "Tools/Nunchaku/nunchaku_collect.ML"
    98.9 -ML_file "Tools/Nunchaku/nunchaku_problem.ML"
   98.10 -ML_file "Tools/Nunchaku/nunchaku_translate.ML"
   98.11 -ML_file "Tools/Nunchaku/nunchaku_model.ML"
   98.12 -ML_file "Tools/Nunchaku/nunchaku_reconstruct.ML"
   98.13 -ML_file "Tools/Nunchaku/nunchaku_display.ML"
   98.14 -ML_file "Tools/Nunchaku/nunchaku_tool.ML"
   98.15 -ML_file "Tools/Nunchaku/nunchaku.ML"
   98.16 -ML_file "Tools/Nunchaku/nunchaku_commands.ML"
   98.17 +ML_file \<open>Tools/Nunchaku/nunchaku_util.ML\<close>
   98.18 +ML_file \<open>Tools/Nunchaku/nunchaku_collect.ML\<close>
   98.19 +ML_file \<open>Tools/Nunchaku/nunchaku_problem.ML\<close>
   98.20 +ML_file \<open>Tools/Nunchaku/nunchaku_translate.ML\<close>
   98.21 +ML_file \<open>Tools/Nunchaku/nunchaku_model.ML\<close>
   98.22 +ML_file \<open>Tools/Nunchaku/nunchaku_reconstruct.ML\<close>
   98.23 +ML_file \<open>Tools/Nunchaku/nunchaku_display.ML\<close>
   98.24 +ML_file \<open>Tools/Nunchaku/nunchaku_tool.ML\<close>
   98.25 +ML_file \<open>Tools/Nunchaku/nunchaku.ML\<close>
   98.26 +ML_file \<open>Tools/Nunchaku/nunchaku_commands.ML\<close>
   98.27  
   98.28  hide_const (open) unreachable The_unsafe rmember
   98.29  
    99.1 --- a/src/HOL/Orderings.thy	Sun Jan 06 13:44:33 2019 +0100
    99.2 +++ b/src/HOL/Orderings.thy	Sun Jan 06 15:04:34 2019 +0100
    99.3 @@ -9,8 +9,8 @@
    99.4  keywords "print_orders" :: diag
    99.5  begin
    99.6  
    99.7 -ML_file "~~/src/Provers/order.ML"
    99.8 -ML_file "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    99.9 +ML_file \<open>~~/src/Provers/order.ML\<close>
   99.10 +ML_file \<open>~~/src/Provers/quasi.ML\<close>  (* FIXME unused? *)
   99.11  
   99.12  subsection \<open>Abstract ordering\<close>
   99.13  
   100.1 --- a/src/HOL/Partial_Function.thy	Sun Jan 06 13:44:33 2019 +0100
   100.2 +++ b/src/HOL/Partial_Function.thy	Sun Jan 06 15:04:34 2019 +0100
   100.3 @@ -10,7 +10,7 @@
   100.4  begin
   100.5  
   100.6  named_theorems partial_function_mono "monotonicity rules for partial function definitions"
   100.7 -ML_file "Tools/Function/partial_function.ML"
   100.8 +ML_file \<open>Tools/Function/partial_function.ML\<close>
   100.9  
  100.10  lemma (in ccpo) in_chain_finite:
  100.11    assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}"
   101.1 --- a/src/HOL/Predicate_Compile.thy	Sun Jan 06 13:44:33 2019 +0100
   101.2 +++ b/src/HOL/Predicate_Compile.thy	Sun Jan 06 15:04:34 2019 +0100
   101.3 @@ -11,17 +11,17 @@
   101.4    "values" :: diag
   101.5  begin
   101.6  
   101.7 -ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"
   101.8 -ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML"
   101.9 -ML_file "Tools/Predicate_Compile/core_data.ML"
  101.10 -ML_file "Tools/Predicate_Compile/mode_inference.ML"
  101.11 -ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML"
  101.12 -ML_file "Tools/Predicate_Compile/predicate_compile_core.ML"
  101.13 -ML_file "Tools/Predicate_Compile/predicate_compile_data.ML"
  101.14 -ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML"
  101.15 -ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML"
  101.16 -ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
  101.17 -ML_file "Tools/Predicate_Compile/predicate_compile.ML"
  101.18 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_aux.ML\<close>
  101.19 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_compilations.ML\<close>
  101.20 +ML_file \<open>Tools/Predicate_Compile/core_data.ML\<close>
  101.21 +ML_file \<open>Tools/Predicate_Compile/mode_inference.ML\<close>
  101.22 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_proof.ML\<close>
  101.23 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_core.ML\<close>
  101.24 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_data.ML\<close>
  101.25 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_fun.ML\<close>
  101.26 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_pred.ML\<close>
  101.27 +ML_file \<open>Tools/Predicate_Compile/predicate_compile_specialisation.ML\<close>
  101.28 +ML_file \<open>Tools/Predicate_Compile/predicate_compile.ML\<close>
  101.29  
  101.30  
  101.31  subsection \<open>Set membership as a generator predicate\<close>
   102.1 --- a/src/HOL/Presburger.thy	Sun Jan 06 13:44:33 2019 +0100
   102.2 +++ b/src/HOL/Presburger.thy	Sun Jan 06 15:04:34 2019 +0100
   102.3 @@ -9,8 +9,8 @@
   102.4  keywords "try0" :: diag
   102.5  begin
   102.6  
   102.7 -ML_file "Tools/Qelim/qelim.ML"
   102.8 -ML_file "Tools/Qelim/cooper_procedure.ML"
   102.9 +ML_file \<open>Tools/Qelim/qelim.ML\<close>
  102.10 +ML_file \<open>Tools/Qelim/cooper_procedure.ML\<close>
  102.11  
  102.12  subsection\<open>The \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Properties\<close>
  102.13  
  102.14 @@ -390,7 +390,7 @@
  102.15    "\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<and> P) = (0 \<le> x' \<and> P')"
  102.16    by (simp cong: conj_cong)
  102.17  
  102.18 -ML_file "Tools/Qelim/cooper.ML"
  102.19 +ML_file \<open>Tools/Qelim/cooper.ML\<close>
  102.20  
  102.21  method_setup presburger = \<open>
  102.22    let
  102.23 @@ -505,6 +505,6 @@
  102.24  
  102.25  subsection \<open>Try0\<close>
  102.26  
  102.27 -ML_file "Tools/try0.ML"
  102.28 +ML_file \<open>Tools/try0.ML\<close>
  102.29  
  102.30  end
   103.1 --- a/src/HOL/Product_Type.thy	Sun Jan 06 13:44:33 2019 +0100
   103.2 +++ b/src/HOL/Product_Type.thy	Sun Jan 06 15:04:34 2019 +0100
   103.3 @@ -738,7 +738,7 @@
   103.4  lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
   103.5    by (simp only: internal_case_prod_def case_prod_conv)
   103.6  
   103.7 -ML_file "Tools/split_rule.ML"
   103.8 +ML_file \<open>Tools/split_rule.ML\<close>
   103.9  
  103.10  hide_const internal_case_prod
  103.11  
  103.12 @@ -1263,7 +1263,7 @@
  103.13  
  103.14  subsection \<open>Simproc for rewriting a set comprehension into a pointfree expression\<close>
  103.15  
  103.16 -ML_file "Tools/set_comprehension_pointfree.ML"
  103.17 +ML_file \<open>Tools/set_comprehension_pointfree.ML\<close>
  103.18  
  103.19  setup \<open>
  103.20    Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
  103.21 @@ -1309,7 +1309,7 @@
  103.22      | _ => NONE)
  103.23  \<close>
  103.24  
  103.25 -ML_file "Tools/inductive_set.ML"
  103.26 +ML_file \<open>Tools/inductive_set.ML\<close>
  103.27  
  103.28  
  103.29  subsection \<open>Legacy theorem bindings and duplicates\<close>
   104.1 --- a/src/HOL/Prolog/HOHH.thy	Sun Jan 06 13:44:33 2019 +0100
   104.2 +++ b/src/HOL/Prolog/HOHH.thy	Sun Jan 06 15:04:34 2019 +0100
   104.3 @@ -8,7 +8,7 @@
   104.4  imports HOL.HOL
   104.5  begin
   104.6  
   104.7 -ML_file "prolog.ML"
   104.8 +ML_file \<open>prolog.ML\<close>
   104.9  
  104.10  method_setup ptac =
  104.11    \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
   105.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 06 13:44:33 2019 +0100
   105.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 06 15:04:34 2019 +0100
   105.3 @@ -705,14 +705,14 @@
   105.4  
   105.5  notation (output) unknown  ("?")
   105.6  
   105.7 -ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   105.8 +ML_file \<open>Tools/Quickcheck/exhaustive_generators.ML\<close>
   105.9  
  105.10  declare [[quickcheck_batch_tester = exhaustive]]
  105.11  
  105.12  
  105.13  subsection \<open>Defining generators for abstract types\<close>
  105.14  
  105.15 -ML_file "Tools/Quickcheck/abstract_generators.ML"
  105.16 +ML_file \<open>Tools/Quickcheck/abstract_generators.ML\<close>
  105.17  
  105.18  hide_fact (open) orelse_def
  105.19  no_notation orelse  (infixr "orelse" 55)
   106.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sun Jan 06 13:44:33 2019 +0100
   106.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Jan 06 15:04:34 2019 +0100
   106.3 @@ -192,9 +192,9 @@
   106.4  
   106.5  subsubsection \<open>Setting up the counterexample generator\<close>
   106.6  
   106.7 -external_file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
   106.8 -external_file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
   106.9 -ML_file "Tools/Quickcheck/narrowing_generators.ML"
  106.10 +external_file \<open>~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\<close>
  106.11 +external_file \<open>~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\<close>
  106.12 +ML_file \<open>Tools/Quickcheck/narrowing_generators.ML\<close>
  106.13  
  106.14  definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
  106.15  where
  106.16 @@ -318,7 +318,7 @@
  106.17  
  106.18  subsection \<open>The \<open>find_unused_assms\<close> command\<close>
  106.19  
  106.20 -ML_file "Tools/Quickcheck/find_unused_assms.ML"
  106.21 +ML_file \<open>Tools/Quickcheck/find_unused_assms.ML\<close>
  106.22  
  106.23  subsection \<open>Closing up\<close>
  106.24  
   107.1 --- a/src/HOL/Quickcheck_Random.thy	Sun Jan 06 13:44:33 2019 +0100
   107.2 +++ b/src/HOL/Quickcheck_Random.thy	Sun Jan 06 15:04:34 2019 +0100
   107.3 @@ -209,8 +209,8 @@
   107.4  
   107.5  subsection \<open>Deriving random generators for datatypes\<close>
   107.6  
   107.7 -ML_file "Tools/Quickcheck/quickcheck_common.ML"
   107.8 -ML_file "Tools/Quickcheck/random_generators.ML"
   107.9 +ML_file \<open>Tools/Quickcheck/quickcheck_common.ML\<close>
  107.10 +ML_file \<open>Tools/Quickcheck/random_generators.ML\<close>
  107.11  
  107.12  
  107.13  subsection \<open>Code setup\<close>
   108.1 --- a/src/HOL/Quotient.thy	Sun Jan 06 13:44:33 2019 +0100
   108.2 +++ b/src/HOL/Quotient.thy	Sun Jan 06 15:04:34 2019 +0100
   108.3 @@ -636,7 +636,7 @@
   108.4    and quot_preserve "preservation theorems"
   108.5    and id_simps "identity simp rules for maps"
   108.6    and quot_thm "quotient theorems"
   108.7 -ML_file "Tools/Quotient/quotient_info.ML"
   108.8 +ML_file \<open>Tools/Quotient/quotient_info.ML\<close>
   108.9  
  108.10  declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
  108.11  
  108.12 @@ -657,15 +657,15 @@
  108.13    vimage_id
  108.14  
  108.15  text \<open>Translation functions for the lifting process.\<close>
  108.16 -ML_file "Tools/Quotient/quotient_term.ML"
  108.17 +ML_file \<open>Tools/Quotient/quotient_term.ML\<close>
  108.18  
  108.19  
  108.20  text \<open>Definitions of the quotient types.\<close>
  108.21 -ML_file "Tools/Quotient/quotient_type.ML"
  108.22 +ML_file \<open>Tools/Quotient/quotient_type.ML\<close>
  108.23  
  108.24  
  108.25  text \<open>Definitions for quotient constants.\<close>
  108.26 -ML_file "Tools/Quotient/quotient_def.ML"
  108.27 +ML_file \<open>Tools/Quotient/quotient_def.ML\<close>
  108.28  
  108.29  
  108.30  text \<open>
  108.31 @@ -692,7 +692,7 @@
  108.32  begin
  108.33  
  108.34  text \<open>Tactics for proving the lifted theorems\<close>
  108.35 -ML_file "Tools/Quotient/quotient_tacs.ML"
  108.36 +ML_file \<open>Tools/Quotient/quotient_tacs.ML\<close>
  108.37  
  108.38  end
  108.39  
   109.1 --- a/src/HOL/Real.thy	Sun Jan 06 13:44:33 2019 +0100
   109.2 +++ b/src/HOL/Real.thy	Sun Jan 06 15:04:34 2019 +0100
   109.3 @@ -1644,8 +1644,8 @@
   109.4  
   109.5  subsection \<open>Setup for SMT\<close>
   109.6  
   109.7 -ML_file "Tools/SMT/smt_real.ML"
   109.8 -ML_file "Tools/SMT/z3_real.ML"
   109.9 +ML_file \<open>Tools/SMT/smt_real.ML\<close>
  109.10 +ML_file \<open>Tools/SMT/z3_real.ML\<close>
  109.11  
  109.12  lemma [z3_rule]:
  109.13    "0 + x = x"
  109.14 @@ -1660,6 +1660,6 @@
  109.15  
  109.16  subsection \<open>Setup for Argo\<close>
  109.17  
  109.18 -ML_file "Tools/Argo/argo_real.ML"
  109.19 +ML_file \<open>Tools/Argo/argo_real.ML\<close>
  109.20  
  109.21  end
   110.1 --- a/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jan 06 13:44:33 2019 +0100
   110.2 +++ b/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jan 06 15:04:34 2019 +0100
   110.3 @@ -3,7 +3,7 @@
   110.4    imports "HOL-Real_Asymp.Real_Asymp"
   110.5  begin
   110.6  
   110.7 -ML_file "~~/src/Doc/antiquote_setup.ML"
   110.8 +ML_file \<open>~~/src/Doc/antiquote_setup.ML\<close>
   110.9  (*>*)
  110.10  
  110.11  section \<open>Introduction\<close>
   111.1 --- a/src/HOL/Record.thy	Sun Jan 06 13:44:33 2019 +0100
   111.2 +++ b/src/HOL/Record.thy	Sun Jan 06 15:04:34 2019 +0100
   111.3 @@ -453,7 +453,7 @@
   111.4  
   111.5  subsection \<open>Record package\<close>
   111.6  
   111.7 -ML_file "Tools/record.ML"
   111.8 +ML_file \<open>Tools/record.ML\<close>
   111.9  
  111.10  hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
  111.11    iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   112.1 --- a/src/HOL/Rings.thy	Sun Jan 06 13:44:33 2019 +0100
   112.2 +++ b/src/HOL/Rings.thy	Sun Jan 06 15:04:34 2019 +0100
   112.3 @@ -1762,9 +1762,9 @@
   112.4  text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
   112.5  
   112.6  named_theorems arith "arith facts -- only ground formulas"
   112.7 -ML_file "Tools/arith_data.ML"
   112.8 -
   112.9 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
  112.10 +ML_file \<open>Tools/arith_data.ML\<close>
  112.11 +
  112.12 +ML_file \<open>~~/src/Provers/Arith/cancel_div_mod.ML\<close>
  112.13  
  112.14  ML \<open>
  112.15  structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
   113.1 --- a/src/HOL/SAT.thy	Sun Jan 06 13:44:33 2019 +0100
   113.2 +++ b/src/HOL/SAT.thy	Sun Jan 06 15:04:34 2019 +0100
   113.3 @@ -11,10 +11,10 @@
   113.4  imports Argo
   113.5  begin
   113.6  
   113.7 -ML_file "Tools/prop_logic.ML"
   113.8 -ML_file "Tools/sat_solver.ML"
   113.9 -ML_file "Tools/sat.ML"
  113.10 -ML_file "Tools/Argo/argo_sat_solver.ML"
  113.11 +ML_file \<open>Tools/prop_logic.ML\<close>
  113.12 +ML_file \<open>Tools/sat_solver.ML\<close>
  113.13 +ML_file \<open>Tools/sat.ML\<close>
  113.14 +ML_file \<open>Tools/Argo/argo_sat_solver.ML\<close>
  113.15  
  113.16  method_setup sat = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\<close>
  113.17    "SAT solver"
   114.1 --- a/src/HOL/SMT.thy	Sun Jan 06 13:44:33 2019 +0100
   114.2 +++ b/src/HOL/SMT.thy	Sun Jan 06 15:04:34 2019 +0100
   114.3 @@ -286,35 +286,35 @@
   114.4  
   114.5  subsection \<open>Setup\<close>
   114.6  
   114.7 -ML_file "Tools/SMT/smt_util.ML"
   114.8 -ML_file "Tools/SMT/smt_failure.ML"
   114.9 -ML_file "Tools/SMT/smt_config.ML"
  114.10 -ML_file "Tools/SMT/smt_builtin.ML"
  114.11 -ML_file "Tools/SMT/smt_datatypes.ML"
  114.12 -ML_file "Tools/SMT/smt_normalize.ML"
  114.13 -ML_file "Tools/SMT/smt_translate.ML"
  114.14 -ML_file "Tools/SMT/smtlib.ML"
  114.15 -ML_file "Tools/SMT/smtlib_interface.ML"
  114.16 -ML_file "Tools/SMT/smtlib_proof.ML"
  114.17 -ML_file "Tools/SMT/smtlib_isar.ML"
  114.18 -ML_file "Tools/SMT/z3_proof.ML"
  114.19 -ML_file "Tools/SMT/z3_isar.ML"
  114.20 -ML_file "Tools/SMT/smt_solver.ML"
  114.21 -ML_file "Tools/SMT/cvc4_interface.ML"
  114.22 -ML_file "Tools/SMT/cvc4_proof_parse.ML"
  114.23 -ML_file "Tools/SMT/verit_proof.ML"
  114.24 -ML_file "Tools/SMT/verit_isar.ML"
  114.25 -ML_file "Tools/SMT/verit_proof_parse.ML"
  114.26 -ML_file "Tools/SMT/conj_disj_perm.ML"
  114.27 -ML_file "Tools/SMT/smt_replay_methods.ML"
  114.28 -ML_file "Tools/SMT/smt_replay.ML"
  114.29 -ML_file "Tools/SMT/z3_interface.ML"
  114.30 -ML_file "Tools/SMT/z3_replay_rules.ML"
  114.31 -ML_file "Tools/SMT/z3_replay_methods.ML"
  114.32 -ML_file "Tools/SMT/z3_replay.ML"
  114.33 -ML_file "Tools/SMT/verit_replay_methods.ML"
  114.34 -ML_file "Tools/SMT/verit_replay.ML"
  114.35 -ML_file "Tools/SMT/smt_systems.ML"
  114.36 +ML_file \<open>Tools/SMT/smt_util.ML\<close>
  114.37 +ML_file \<open>Tools/SMT/smt_failure.ML\<close>
  114.38 +ML_file \<open>Tools/SMT/smt_config.ML\<close>
  114.39 +ML_file \<open>Tools/SMT/smt_builtin.ML\<close>
  114.40 +ML_file \<open>Tools/SMT/smt_datatypes.ML\<close>
  114.41 +ML_file \<open>Tools/SMT/smt_normalize.ML\<close>
  114.42 +ML_file \<open>Tools/SMT/smt_translate.ML\<close>
  114.43 +ML_file \<open>Tools/SMT/smtlib.ML\<close>
  114.44 +ML_file \<open>Tools/SMT/smtlib_interface.ML\<close>
  114.45 +ML_file \<open>Tools/SMT/smtlib_proof.ML\<close>
  114.46 +ML_file \<open>Tools/SMT/smtlib_isar.ML\<close>
  114.47 +ML_file \<open>Tools/SMT/z3_proof.ML\<close>
  114.48 +ML_file \<open>Tools/SMT/z3_isar.ML\<close>
  114.49 +ML_file \<open>Tools/SMT/smt_solver.ML\<close>
  114.50 +ML_file \<open>Tools/SMT/cvc4_interface.ML\<close>
  114.51 +ML_file \<open>Tools/SMT/cvc4_proof_parse.ML\<close>
  114.52 +ML_file \<open>Tools/SMT/verit_proof.ML\<close>
  114.53 +ML_file \<open>Tools/SMT/verit_isar.ML\<close>
  114.54 +ML_file \<open>Tools/SMT/verit_proof_parse.ML\<close>
  114.55 +ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close>
  114.56 +ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close>
  114.57 +ML_file \<open>Tools/SMT/smt_replay.ML\<close>
  114.58 +ML_file \<open>Tools/SMT/z3_interface.ML\<close>
  114.59 +ML_file \<open>Tools/SMT/z3_replay_rules.ML\<close>
  114.60 +ML_file \<open>Tools/SMT/z3_replay_methods.ML\<close>
  114.61 +ML_file \<open>Tools/SMT/z3_replay.ML\<close>
  114.62 +ML_file \<open>Tools/SMT/verit_replay_methods.ML\<close>
  114.63 +ML_file \<open>Tools/SMT/verit_replay.ML\<close>
  114.64 +ML_file \<open>Tools/SMT/smt_systems.ML\<close>
  114.65  
  114.66  method_setup smt = \<open>
  114.67    Scan.optional Attrib.thms [] >>
   115.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Sun Jan 06 13:44:33 2019 +0100
   115.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Sun Jan 06 15:04:34 2019 +0100
   115.3 @@ -45,7 +45,7 @@
   115.4  
   115.5  section \<open>Setup\<close>
   115.6  
   115.7 -ML_file "boogie.ML"
   115.8 +ML_file \<open>boogie.ML\<close>
   115.9  
  115.10  
  115.11  
  115.12 @@ -55,22 +55,22 @@
  115.13  declare [[smt_read_only_certificates = true]]
  115.14  
  115.15  
  115.16 -external_file "Boogie_Max.certs"
  115.17 +external_file \<open>Boogie_Max.certs\<close>
  115.18  declare [[smt_certificates = "Boogie_Max.certs"]]
  115.19  
  115.20 -boogie_file Boogie_Max
  115.21 +boogie_file \<open>Boogie_Max\<close>
  115.22  
  115.23  
  115.24 -external_file "Boogie_Dijkstra.certs"
  115.25 +external_file \<open>Boogie_Dijkstra.certs\<close>
  115.26  declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
  115.27  
  115.28 -boogie_file Boogie_Dijkstra
  115.29 +boogie_file \<open>Boogie_Dijkstra\<close>
  115.30  
  115.31  
  115.32  declare [[z3_extensions = true]]
  115.33 -external_file "VCC_Max.certs"
  115.34 +external_file \<open>VCC_Max.certs\<close>
  115.35  declare [[smt_certificates = "VCC_Max.certs"]]
  115.36  
  115.37 -boogie_file VCC_Max
  115.38 +boogie_file \<open>VCC_Max\<close>
  115.39  
  115.40  end
   116.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jan 06 13:44:33 2019 +0100
   116.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jan 06 15:04:34 2019 +0100
   116.3 @@ -8,7 +8,7 @@
   116.4  imports Complex_Main
   116.5  begin
   116.6  
   116.7 -external_file "SMT_Examples.certs"
   116.8 +external_file \<open>SMT_Examples.certs\<close>
   116.9  declare [[smt_certificates = "SMT_Examples.certs"]]
  116.10  declare [[smt_read_only_certificates = true]]
  116.11  
   117.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Jan 06 13:44:33 2019 +0100
   117.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Jan 06 15:04:34 2019 +0100
   117.3 @@ -10,7 +10,7 @@
   117.4  spark_proof_functions
   117.5    gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
   117.6  
   117.7 -spark_open "greatest_common_divisor/g_c_d"
   117.8 +spark_open \<open>greatest_common_divisor/g_c_d\<close>
   117.9  
  117.10  spark_vc procedure_g_c_d_4
  117.11  proof -
   118.1 --- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Sun Jan 06 13:44:33 2019 +0100
   118.2 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Sun Jan 06 15:04:34 2019 +0100
   118.3 @@ -541,7 +541,7 @@
   118.4  
   118.5  text \<open>The verification conditions\<close>
   118.6  
   118.7 -spark_open "liseq/liseq_length"
   118.8 +spark_open \<open>liseq/liseq_length\<close>
   118.9  
  118.10  spark_vc procedure_liseq_length_5
  118.11    by (simp_all add: liseq_singleton liseq'_singleton)
   119.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sun Jan 06 13:44:33 2019 +0100
   119.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sun Jan 06 15:04:34 2019 +0100
   119.3 @@ -8,7 +8,7 @@
   119.4  imports RMD_Specification
   119.5  begin
   119.6  
   119.7 -spark_open "rmd/f"
   119.8 +spark_open \<open>rmd/f\<close>
   119.9  
  119.10  spark_vc function_f_2
  119.11    using assms by simp_all
   120.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy	Sun Jan 06 13:44:33 2019 +0100
   120.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy	Sun Jan 06 15:04:34 2019 +0100
   120.3 @@ -8,7 +8,7 @@
   120.4  imports RMD_Specification
   120.5  begin
   120.6  
   120.7 -spark_open "rmd/hash"
   120.8 +spark_open \<open>rmd/hash\<close>
   120.9  
  120.10  abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
  120.11    "from_chain c \<equiv> (
   121.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy	Sun Jan 06 13:44:33 2019 +0100
   121.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy	Sun Jan 06 15:04:34 2019 +0100
   121.3 @@ -8,7 +8,7 @@
   121.4  imports RMD_Specification
   121.5  begin
   121.6  
   121.7 -spark_open "rmd/k_l"
   121.8 +spark_open \<open>rmd/k_l\<close>
   121.9  
  121.10  spark_vc function_k_l_6
  121.11    using assms by (simp add: K_def)
   122.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy	Sun Jan 06 13:44:33 2019 +0100
   122.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy	Sun Jan 06 15:04:34 2019 +0100
   122.3 @@ -8,7 +8,7 @@
   122.4  imports RMD_Specification
   122.5  begin
   122.6  
   122.7 -spark_open "rmd/k_r"
   122.8 +spark_open \<open>rmd/k_r\<close>
   122.9  
  122.10  spark_vc function_k_r_6
  122.11    using assms by (simp add: K'_def)
   123.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy	Sun Jan 06 13:44:33 2019 +0100
   123.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy	Sun Jan 06 15:04:34 2019 +0100
   123.3 @@ -8,7 +8,7 @@
   123.4  imports RMD_Specification RMD_Lemmas
   123.5  begin
   123.6  
   123.7 -spark_open "rmd/r_l"
   123.8 +spark_open \<open>rmd/r_l\<close>
   123.9  
  123.10  spark_vc function_r_l_2
  123.11  proof -
   124.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy	Sun Jan 06 13:44:33 2019 +0100
   124.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy	Sun Jan 06 15:04:34 2019 +0100
   124.3 @@ -8,7 +8,7 @@
   124.4  imports RMD_Specification RMD_Lemmas
   124.5  begin
   124.6  
   124.7 -spark_open "rmd/r_r"
   124.8 +spark_open \<open>rmd/r_r\<close>
   124.9  
  124.10  spark_vc function_r_r_2
  124.11  proof -
   125.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sun Jan 06 13:44:33 2019 +0100
   125.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sun Jan 06 15:04:34 2019 +0100
   125.3 @@ -8,7 +8,7 @@
   125.4  imports RMD_Specification
   125.5  begin
   125.6  
   125.7 -spark_open "rmd/round"
   125.8 +spark_open \<open>rmd/round\<close>
   125.9  
  125.10  abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
  125.11    "from_chain c \<equiv> (
   126.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy	Sun Jan 06 13:44:33 2019 +0100
   126.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy	Sun Jan 06 15:04:34 2019 +0100
   126.3 @@ -8,7 +8,7 @@
   126.4  imports RMD_Specification RMD_Lemmas
   126.5  begin
   126.6  
   126.7 -spark_open "rmd/s_l"
   126.8 +spark_open \<open>rmd/s_l\<close>
   126.9  
  126.10  spark_vc function_s_l_2
  126.11  proof -
   127.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy	Sun Jan 06 13:44:33 2019 +0100
   127.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy	Sun Jan 06 15:04:34 2019 +0100
   127.3 @@ -8,7 +8,7 @@
   127.4  imports RMD_Specification RMD_Lemmas
   127.5  begin
   127.6  
   127.7 -spark_open "rmd/s_r"
   127.8 +spark_open \<open>rmd/s_r\<close>
   127.9  
  127.10  spark_vc function_s_r_2
  127.11  proof -
   128.1 --- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Sun Jan 06 13:44:33 2019 +0100
   128.2 +++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Sun Jan 06 15:04:34 2019 +0100
   128.3 @@ -7,7 +7,7 @@
   128.4  imports "HOL-SPARK.SPARK"
   128.5  begin
   128.6  
   128.7 -spark_open "sqrt/isqrt"
   128.8 +spark_open \<open>sqrt/isqrt\<close>
   128.9  
  128.10  spark_vc function_isqrt_4
  128.11  proof -
   129.1 --- a/src/HOL/SPARK/Manual/Complex_Types.thy	Sun Jan 06 13:44:33 2019 +0100
   129.2 +++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Sun Jan 06 15:04:34 2019 +0100
   129.3 @@ -31,7 +31,7 @@
   129.4    complex_types__initialized3 = initialized3
   129.5  
   129.6  (*<*)
   129.7 -spark_open "complex_types_app/initialize"
   129.8 +spark_open \<open>complex_types_app/initialize\<close>
   129.9  
  129.10  spark_vc procedure_initialize_1
  129.11    by (simp add: initialized_def)
   130.1 --- a/src/HOL/SPARK/Manual/Proc1.thy	Sun Jan 06 13:44:33 2019 +0100
   130.2 +++ b/src/HOL/SPARK/Manual/Proc1.thy	Sun Jan 06 15:04:34 2019 +0100
   130.3 @@ -2,7 +2,7 @@
   130.4  imports "HOL-SPARK.SPARK"
   130.5  begin
   130.6  
   130.7 -spark_open "loop_invariant/proc1"
   130.8 +spark_open \<open>loop_invariant/proc1\<close>
   130.9  
  130.10  spark_vc procedure_proc1_5
  130.11    by (simp add: ring_distribs mod_simps)
   131.1 --- a/src/HOL/SPARK/Manual/Proc2.thy	Sun Jan 06 13:44:33 2019 +0100
   131.2 +++ b/src/HOL/SPARK/Manual/Proc2.thy	Sun Jan 06 15:04:34 2019 +0100
   131.3 @@ -2,7 +2,7 @@
   131.4  imports "HOL-SPARK.SPARK"
   131.5  begin
   131.6  
   131.7 -spark_open "loop_invariant/proc2"
   131.8 +spark_open \<open>loop_invariant/proc2\<close>
   131.9  
  131.10  spark_vc procedure_proc2_7
  131.11    by (simp add: ring_distribs mod_simps)
   132.1 --- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sun Jan 06 13:44:33 2019 +0100
   132.2 +++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sun Jan 06 15:04:34 2019 +0100
   132.3 @@ -10,7 +10,7 @@
   132.4  spark_proof_functions
   132.5    gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
   132.6  
   132.7 -spark_open "simple_greatest_common_divisor/g_c_d"
   132.8 +spark_open \<open>simple_greatest_common_divisor/g_c_d\<close>
   132.9  
  132.10  spark_vc procedure_g_c_d_4
  132.11    using \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>
   133.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Sun Jan 06 13:44:33 2019 +0100
   133.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Sun Jan 06 15:04:34 2019 +0100
   133.3 @@ -15,8 +15,8 @@
   133.4    "spark_status" :: diag
   133.5  begin
   133.6  
   133.7 -ML_file "Tools/fdl_lexer.ML"
   133.8 -ML_file "Tools/fdl_parser.ML"
   133.9 +ML_file \<open>Tools/fdl_lexer.ML\<close>
  133.10 +ML_file \<open>Tools/fdl_parser.ML\<close>
  133.11  
  133.12  text \<open>
  133.13  SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
  133.14 @@ -181,7 +181,7 @@
  133.15  
  133.16  text \<open>Load the package\<close>
  133.17  
  133.18 -ML_file "Tools/spark_vcs.ML"
  133.19 -ML_file "Tools/spark_commands.ML"
  133.20 +ML_file \<open>Tools/spark_vcs.ML\<close>
  133.21 +ML_file \<open>Tools/spark_commands.ML\<close>
  133.22  
  133.23  end
   134.1 --- a/src/HOL/Semiring_Normalization.thy	Sun Jan 06 13:44:33 2019 +0100
   134.2 +++ b/src/HOL/Semiring_Normalization.thy	Sun Jan 06 15:04:34 2019 +0100
   134.3 @@ -67,7 +67,7 @@
   134.4  
   134.5  text \<open>Semiring normalization proper\<close>
   134.6  
   134.7 -ML_file "Tools/semiring_normalizer.ML"
   134.8 +ML_file \<open>Tools/semiring_normalizer.ML\<close>
   134.9  
  134.10  context comm_semiring_1
  134.11  begin
   135.1 --- a/src/HOL/Sledgehammer.thy	Sun Jan 06 13:44:33 2019 +0100
   135.2 +++ b/src/HOL/Sledgehammer.thy	Sun Jan 06 15:04:34 2019 +0100
   135.3 @@ -16,23 +16,23 @@
   135.4  lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
   135.5    by (erule contrapos_nn) (rule arg_cong)
   135.6  
   135.7 -ML_file "Tools/Sledgehammer/async_manager_legacy.ML"
   135.8 -ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
   135.9 -ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
  135.10 -ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML"
  135.11 -ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
  135.12 -ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
  135.13 -ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
  135.14 -ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
  135.15 -ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
  135.16 -ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
  135.17 -ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
  135.18 -ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
  135.19 -ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
  135.20 -ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
  135.21 -ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
  135.22 -ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
  135.23 -ML_file "Tools/Sledgehammer/sledgehammer.ML"
  135.24 -ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
  135.25 +ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
  135.26 +ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
  135.27 +ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
  135.28 +ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
  135.29 +ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
  135.30 +ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
  135.31 +ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
  135.32 +ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
  135.33 +ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
  135.34 +ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
  135.35 +ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
  135.36 +ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
  135.37 +ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
  135.38 +ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
  135.39 +ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
  135.40 +ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
  135.41 +ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
  135.42 +ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
  135.43  
  135.44  end
   136.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Sun Jan 06 13:44:33 2019 +0100
   136.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sun Jan 06 15:04:34 2019 +0100
   136.3 @@ -630,6 +630,6 @@
   136.4  text \<open>Now we have all the theorems in place that are needed for the
   136.5  certificate generating ML functions.\<close>
   136.6  
   136.7 -ML_file "distinct_tree_prover.ML"
   136.8 +ML_file \<open>distinct_tree_prover.ML\<close>
   136.9  
  136.10  end
   137.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Sun Jan 06 13:44:33 2019 +0100
   137.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Sun Jan 06 15:04:34 2019 +0100
   137.3 @@ -8,8 +8,8 @@
   137.4  keywords "statespace" :: thy_decl
   137.5  begin
   137.6  
   137.7 -ML_file "state_space.ML"
   137.8 -ML_file "state_fun.ML"
   137.9 +ML_file \<open>state_space.ML\<close>
  137.10 +ML_file \<open>state_fun.ML\<close>
  137.11  
  137.12  text \<open>For every type that is to be stored in a state space, an
  137.13  instance of this locale is imported in order convert the abstract and
   138.1 --- a/src/HOL/String.thy	Sun Jan 06 13:44:33 2019 +0100
   138.2 +++ b/src/HOL/String.thy	Sun Jan 06 15:04:34 2019 +0100
   138.3 @@ -200,7 +200,7 @@
   138.4  syntax
   138.5    "_String" :: "str_position \<Rightarrow> string"    ("_")
   138.6  
   138.7 -ML_file "Tools/string_syntax.ML"
   138.8 +ML_file \<open>Tools/string_syntax.ML\<close>
   138.9  
  138.10  instantiation char :: enum
  138.11  begin
  138.12 @@ -458,7 +458,7 @@
  138.13    "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
  138.14    "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
  138.15  
  138.16 -ML_file "Tools/literal.ML"
  138.17 +ML_file \<open>Tools/literal.ML\<close>
  138.18  
  138.19  
  138.20  subsubsection \<open>Operations\<close>
   139.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jan 06 13:44:33 2019 +0100
   139.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jan 06 15:04:34 2019 +0100
   139.3 @@ -8,7 +8,7 @@
   139.4  imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
   139.5  begin
   139.6  
   139.7 -ML_file "sledgehammer_tactics.ML"
   139.8 +ML_file \<open>sledgehammer_tactics.ML\<close>
   139.9  
  139.10  ML \<open>Proofterm.proofs := 0\<close>
  139.11  
  139.12 @@ -18,7 +18,7 @@
  139.13  declare [[unify_search_bound = 60]]
  139.14  declare [[unify_trace_bound = 60]]
  139.15  
  139.16 -ML_file "atp_problem_import.ML"
  139.17 +ML_file \<open>atp_problem_import.ML\<close>
  139.18  
  139.19  (*
  139.20  ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
   140.1 --- a/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Jan 06 13:44:33 2019 +0100
   140.2 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Jan 06 15:04:34 2019 +0100
   140.3 @@ -8,7 +8,7 @@
   140.4  imports Complex_Main
   140.5  begin
   140.6  
   140.7 -ML_file "atp_theory_export.ML"
   140.8 +ML_file \<open>atp_theory_export.ML\<close>
   140.9  
  140.10  ML \<open>
  140.11  open ATP_Problem
   141.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Sun Jan 06 13:44:33 2019 +0100
   141.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Sun Jan 06 15:04:34 2019 +0100
   141.3 @@ -8,7 +8,7 @@
   141.4  imports MaSh_Export_Base
   141.5  begin
   141.6  
   141.7 -ML_file "mash_eval.ML"
   141.8 +ML_file \<open>mash_eval.ML\<close>
   141.9  
  141.10  sledgehammer_params
  141.11    [provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
   142.1 --- a/src/HOL/TPTP/MaSh_Export_Base.thy	Sun Jan 06 13:44:33 2019 +0100
   142.2 +++ b/src/HOL/TPTP/MaSh_Export_Base.thy	Sun Jan 06 15:04:34 2019 +0100
   142.3 @@ -8,7 +8,7 @@
   142.4  imports Main
   142.5  begin
   142.6  
   142.7 -ML_file "mash_export.ML"
   142.8 +ML_file \<open>mash_export.ML\<close>
   142.9  
  142.10  sledgehammer_params
  142.11    [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
   143.1 --- a/src/HOL/TPTP/TPTP_Interpret.thy	Sun Jan 06 13:44:33 2019 +0100
   143.2 +++ b/src/HOL/TPTP/TPTP_Interpret.thy	Sun Jan 06 15:04:34 2019 +0100
   143.3 @@ -12,6 +12,6 @@
   143.4  
   143.5  typedecl ind
   143.6  
   143.7 -ML_file "TPTP_Parser/tptp_interpret.ML"
   143.8 +ML_file \<open>TPTP_Parser/tptp_interpret.ML\<close>
   143.9  
  143.10  end
   144.1 --- a/src/HOL/TPTP/TPTP_Parser.thy	Sun Jan 06 13:44:33 2019 +0100
   144.2 +++ b/src/HOL/TPTP/TPTP_Parser.thy	Sun Jan 06 15:04:34 2019 +0100
   144.3 @@ -8,13 +8,13 @@
   144.4  imports Pure
   144.5  begin
   144.6  
   144.7 -ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
   144.8 +ML_file \<open>TPTP_Parser/ml_yacc_lib.ML\<close> (*generated from ML-Yacc's lib*)
   144.9  
  144.10 -ML_file "TPTP_Parser/tptp_syntax.ML"
  144.11 -ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
  144.12 -ML_file "TPTP_Parser/tptp_parser.ML"
  144.13 -ML_file "TPTP_Parser/tptp_problem_name.ML"
  144.14 -ML_file "TPTP_Parser/tptp_proof.ML"
  144.15 +ML_file \<open>TPTP_Parser/tptp_syntax.ML\<close>
  144.16 +ML_file \<open>TPTP_Parser/tptp_lexyacc.ML\<close> (*generated from tptp.lex and tptp.yacc*)
  144.17 +ML_file \<open>TPTP_Parser/tptp_parser.ML\<close>
  144.18 +ML_file \<open>TPTP_Parser/tptp_problem_name.ML\<close>
  144.19 +ML_file \<open>TPTP_Parser/tptp_proof.ML\<close>
  144.20  
  144.21  text \<open>The TPTP parser was generated using ML-Yacc, and needs the
  144.22  ML-Yacc library to operate.  This library is included with the parser,
   145.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jan 06 13:44:33 2019 +0100
   145.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jan 06 15:04:34 2019 +0100
   145.3 @@ -75,9 +75,9 @@
   145.4    tptp_informative_failure = true
   145.5  ]]
   145.6  
   145.7 -ML_file "TPTP_Parser/tptp_reconstruct_library.ML"
   145.8 +ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close>
   145.9  ML "open TPTP_Reconstruct_Library"
  145.10 -ML_file "TPTP_Parser/tptp_reconstruct.ML"
  145.11 +ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close>
  145.12  
  145.13  (*FIXME fudge*)
  145.14  declare [[
   146.1 --- a/src/HOL/Transfer.thy	Sun Jan 06 13:44:33 2019 +0100
   146.2 +++ b/src/HOL/Transfer.thy	Sun Jan 06 15:04:34 2019 +0100
   146.3 @@ -230,7 +230,7 @@
   146.4  
   146.5  
   146.6  
   146.7 -ML_file "Tools/Transfer/transfer.ML"
   146.8 +ML_file \<open>Tools/Transfer/transfer.ML\<close>
   146.9  declare refl [transfer_rule]
  146.10  
  146.11  hide_const (open) Rel
  146.12 @@ -362,8 +362,8 @@
  146.13    "(if \<not> P then t else e) = (if P then e else t)"
  146.14  by auto
  146.15  
  146.16 -ML_file "Tools/Transfer/transfer_bnf.ML"
  146.17 -ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
  146.18 +ML_file \<open>Tools/Transfer/transfer_bnf.ML\<close>
  146.19 +ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_transfer.ML\<close>
  146.20  
  146.21  declare pred_fun_def [simp]
  146.22  declare rel_fun_eq [relator_eq]
   147.1 --- a/src/HOL/Transitive_Closure.thy	Sun Jan 06 13:44:33 2019 +0100
   147.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Jan 06 15:04:34 2019 +0100
   147.3 @@ -12,7 +12,7 @@
   147.4      and "^=" = "\<^sup>=" "\<^sup>=\<^sup>="
   147.5  begin
   147.6  
   147.7 -ML_file "~~/src/Provers/trancl.ML"
   147.8 +ML_file \<open>~~/src/Provers/trancl.ML\<close>
   147.9  
  147.10  text \<open>
  147.11    \<open>rtrancl\<close> is reflexive/transitive closure,
   148.1 --- a/src/HOL/Typedef.thy	Sun Jan 06 13:44:33 2019 +0100
   148.2 +++ b/src/HOL/Typedef.thy	Sun Jan 06 15:04:34 2019 +0100
   148.3 @@ -108,6 +108,6 @@
   148.4  
   148.5  end
   148.6  
   148.7 -ML_file "Tools/typedef.ML"
   148.8 +ML_file \<open>Tools/typedef.ML\<close>
   148.9  
  148.10  end
   149.1 --- a/src/HOL/Types_To_Sets/Types_To_Sets.thy	Sun Jan 06 13:44:33 2019 +0100
   149.2 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Sun Jan 06 15:04:34 2019 +0100
   149.3 @@ -16,13 +16,13 @@
   149.4  subsection \<open>Rules\<close>
   149.5  
   149.6  text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
   149.7 -ML_file "local_typedef.ML"
   149.8 +ML_file \<open>local_typedef.ML\<close>
   149.9  
  149.10  text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
  149.11 -ML_file "unoverloading.ML"
  149.12 +ML_file \<open>unoverloading.ML\<close>
  149.13  
  149.14  text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
  149.15 -ML_file "internalize_sort.ML"
  149.16 +ML_file \<open>internalize_sort.ML\<close>
  149.17  
  149.18  text\<open>The following file provides some automation to unoverload and internalize the parameters o
  149.19    the sort constraints of a type variable.\<close>
   150.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Sun Jan 06 13:44:33 2019 +0100
   150.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Sun Jan 06 15:04:34 2019 +0100
   150.3 @@ -9,7 +9,7 @@
   150.4  imports Detects PPROD Follows ProgressSets
   150.5  begin
   150.6  
   150.7 -ML_file "UNITY_tactics.ML"
   150.8 +ML_file \<open>UNITY_tactics.ML\<close>
   150.9  
  150.10  method_setup safety = \<open>
  150.11      Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close>
   151.1 --- a/src/HOL/Word/Word.thy	Sun Jan 06 13:44:33 2019 +0100
   151.2 +++ b/src/HOL/Word/Word.thy	Sun Jan 06 15:04:34 2019 +0100
   151.3 @@ -4502,8 +4502,8 @@
   151.4  
   151.5  declare bin_to_bl_def [simp]
   151.6  
   151.7 -ML_file "Tools/word_lib.ML"
   151.8 -ML_file "Tools/smt_word.ML"
   151.9 +ML_file \<open>Tools/word_lib.ML\<close>
  151.10 +ML_file \<open>Tools/smt_word.ML\<close>
  151.11  
  151.12  hide_const (open) Word
  151.13  
   152.1 --- a/src/Sequents/LK.thy	Sun Jan 06 13:44:33 2019 +0100
   152.2 +++ b/src/Sequents/LK.thy	Sun Jan 06 15:04:34 2019 +0100
   152.3 @@ -200,7 +200,7 @@
   152.4  lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x"
   152.5    by (fast add!: subst)
   152.6  
   152.7 -ML_file "simpdata.ML"
   152.8 +ML_file \<open>simpdata.ML\<close>
   152.9  setup \<open>map_theory_simpset (put_simpset LK_ss)\<close>
  152.10  setup \<open>Simplifier.method_setup []\<close>
  152.11  
   153.1 --- a/src/Sequents/Modal0.thy	Sun Jan 06 13:44:33 2019 +0100
   153.2 +++ b/src/Sequents/Modal0.thy	Sun Jan 06 15:04:34 2019 +0100
   153.3 @@ -7,7 +7,7 @@
   153.4  imports LK0
   153.5  begin
   153.6  
   153.7 -ML_file "modal.ML"
   153.8 +ML_file \<open>modal.ML\<close>
   153.9  
  153.10  consts
  153.11    box           :: "o\<Rightarrow>o"       ("[]_" [50] 50)
   154.1 --- a/src/Sequents/Sequents.thy	Sun Jan 06 13:44:33 2019 +0100
   154.2 +++ b/src/Sequents/Sequents.thy	Sun Jan 06 15:04:34 2019 +0100
   154.3 @@ -144,6 +144,6 @@
   154.4  
   154.5  subsection \<open>Proof tools\<close>
   154.6  
   154.7 -ML_file "prover.ML"
   154.8 +ML_file \<open>prover.ML\<close>
   154.9  
  154.10  end
   155.1 --- a/src/Tools/Code_Generator.thy	Sun Jan 06 13:44:33 2019 +0100
   155.2 +++ b/src/Tools/Code_Generator.thy	Sun Jan 06 15:04:34 2019 +0100
   155.3 @@ -16,17 +16,17 @@
   155.4      :: quasi_command
   155.5  begin
   155.6  
   155.7 -ML_file "~~/src/Tools/cache_io.ML"
   155.8 -ML_file "~~/src/Tools/Code/code_preproc.ML"
   155.9 -ML_file "~~/src/Tools/Code/code_symbol.ML"
  155.10 -ML_file "~~/src/Tools/Code/code_thingol.ML"
  155.11 -ML_file "~~/src/Tools/Code/code_simp.ML"
  155.12 -ML_file "~~/src/Tools/Code/code_printer.ML"
  155.13 -ML_file "~~/src/Tools/Code/code_target.ML"
  155.14 -ML_file "~~/src/Tools/Code/code_namespace.ML"
  155.15 -ML_file "~~/src/Tools/Code/code_ml.ML"
  155.16 -ML_file "~~/src/Tools/Code/code_haskell.ML"
  155.17 -ML_file "~~/src/Tools/Code/code_scala.ML"
  155.18 +ML_file \<open>~~/src/Tools/cache_io.ML\<close>
  155.19 +ML_file \<open>~~/src/Tools/Code/code_preproc.ML\<close>
  155.20 +ML_file \<open>~~/src/Tools/Code/code_symbol.ML\<close>
  155.21 +ML_file \<open>~~/src/Tools/Code/code_thingol.ML\<close>
  155.22 +ML_file \<open>~~/src/Tools/Code/code_simp.ML\<close>
  155.23 +ML_file \<open>~~/src/Tools/Code/code_printer.ML\<close>
  155.24 +ML_file \<open>~~/src/Tools/Code/code_target.ML\<close>
  155.25 +ML_file \<open>~~/src/Tools/Code/code_namespace.ML\<close>
  155.26 +ML_file \<open>~~/src/Tools/Code/code_ml.ML\<close>
  155.27 +ML_file \<open>~~/src/Tools/Code/code_haskell.ML\<close>
  155.28 +ML_file \<open>~~/src/Tools/Code/code_scala.ML\<close>
  155.29  
  155.30  code_datatype "TYPE('a::{})"
  155.31  
  155.32 @@ -55,8 +55,8 @@
  155.33      by rule (rule holds)+
  155.34  qed  
  155.35  
  155.36 -ML_file "~~/src/Tools/Code/code_runtime.ML"
  155.37 -ML_file "~~/src/Tools/nbe.ML"
  155.38 +ML_file \<open>~~/src/Tools/Code/code_runtime.ML\<close>
  155.39 +ML_file \<open>~~/src/Tools/nbe.ML\<close>
  155.40  
  155.41  hide_const (open) holds
  155.42  
   156.1 --- a/src/Tools/SML/Examples.thy	Sun Jan 06 13:44:33 2019 +0100
   156.2 +++ b/src/Tools/SML/Examples.thy	Sun Jan 06 15:04:34 2019 +0100
   156.3 @@ -21,7 +21,7 @@
   156.4    evaluates it for some arguments.
   156.5  \<close>
   156.6  
   156.7 -SML_file "factorial.sml"
   156.8 +SML_file \<open>factorial.sml\<close>
   156.9  
  156.10  text \<open>
  156.11    The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands
  156.12 @@ -30,8 +30,8 @@
  156.13    independently of the Isabelle/ML environment.
  156.14  \<close>
  156.15  
  156.16 -SML_file "Example.sig"
  156.17 -SML_file "Example.sml"
  156.18 +SML_file \<open>Example.sig\<close>
  156.19 +SML_file \<open>Example.sml\<close>
  156.20  
  156.21  
  156.22  text \<open>
   157.1 --- a/src/Tools/Spec_Check/Spec_Check.thy	Sun Jan 06 13:44:33 2019 +0100
   157.2 +++ b/src/Tools/Spec_Check/Spec_Check.thy	Sun Jan 06 15:04:34 2019 +0100
   157.3 @@ -2,12 +2,12 @@
   157.4  imports Pure
   157.5  begin
   157.6  
   157.7 -ML_file "random.ML"
   157.8 -ML_file "property.ML"
   157.9 -ML_file "base_generator.ML"
  157.10 -ML_file "generator.ML"
  157.11 -ML_file "gen_construction.ML"
  157.12 -ML_file "spec_check.ML"
  157.13 -ML_file "output_style.ML"
  157.14 +ML_file \<open>random.ML\<close>
  157.15 +ML_file \<open>property.ML\<close>
  157.16 +ML_file \<open>base_generator.ML\<close>
  157.17 +ML_file \<open>generator.ML\<close>
  157.18 +ML_file \<open>gen_construction.ML\<close>
  157.19 +ML_file \<open>spec_check.ML\<close>
  157.20 +ML_file \<open>output_style.ML\<close>
  157.21  
  157.22  end
  157.23 \ No newline at end of file
   158.1 --- a/src/ZF/ArithSimp.thy	Sun Jan 06 13:44:33 2019 +0100
   158.2 +++ b/src/ZF/ArithSimp.thy	Sun Jan 06 15:04:34 2019 +0100
   158.3 @@ -9,9 +9,9 @@
   158.4  imports Arith
   158.5  begin
   158.6  
   158.7 -ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
   158.8 -ML_file "~~/src/Provers/Arith/combine_numerals.ML"
   158.9 -ML_file "arith_data.ML"
  158.10 +ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
  158.11 +ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
  158.12 +ML_file \<open>arith_data.ML\<close>
  158.13  
  158.14  
  158.15  subsection\<open>Difference\<close>
   159.1 --- a/src/ZF/Bin.thy	Sun Jan 06 13:44:33 2019 +0100
   159.2 +++ b/src/ZF/Bin.thy	Sun Jan 06 15:04:34 2019 +0100
   159.3 @@ -117,7 +117,7 @@
   159.4    "_Int" :: "num_token => i"  (\<open>#_\<close> 1000)
   159.5    "_Neg_Int" :: "num_token => i"  (\<open>#-_\<close> 1000)
   159.6  
   159.7 -ML_file "Tools/numeral_syntax.ML"
   159.8 +ML_file \<open>Tools/numeral_syntax.ML\<close>
   159.9  
  159.10  
  159.11  declare bin.intros [simp,TC]
  159.12 @@ -698,7 +698,7 @@
  159.13    apply (simp add: zadd_ac)
  159.14    done
  159.15  
  159.16 -ML_file "int_arith.ML"
  159.17 +ML_file \<open>int_arith.ML\<close>
  159.18  
  159.19  subsection \<open>examples:\<close>
  159.20  
   160.1 --- a/src/ZF/Datatype.thy	Sun Jan 06 13:44:33 2019 +0100
   160.2 +++ b/src/ZF/Datatype.thy	Sun Jan 06 15:04:34 2019 +0100
   160.3 @@ -10,7 +10,7 @@
   160.4  keywords "datatype" "codatatype" :: thy_decl
   160.5  begin
   160.6  
   160.7 -ML_file "Tools/datatype_package.ML"
   160.8 +ML_file \<open>Tools/datatype_package.ML\<close>
   160.9  
  160.10  ML \<open>
  160.11  (*Typechecking rules for most datatypes involving univ*)
   161.1 --- a/src/ZF/Inductive.thy	Sun Jan 06 13:44:33 2019 +0100
   161.2 +++ b/src/ZF/Inductive.thy	Sun Jan 06 15:04:34 2019 +0100
   161.3 @@ -27,12 +27,12 @@
   161.4  
   161.5  lemma refl_thin: "!!P. a = a ==> P ==> P" .
   161.6  
   161.7 -ML_file "ind_syntax.ML"
   161.8 -ML_file "Tools/ind_cases.ML"
   161.9 -ML_file "Tools/cartprod.ML"
  161.10 -ML_file "Tools/inductive_package.ML"
  161.11 -ML_file "Tools/induct_tacs.ML"
  161.12 -ML_file "Tools/primrec_package.ML"
  161.13 +ML_file \<open>ind_syntax.ML\<close>
  161.14 +ML_file \<open>Tools/ind_cases.ML\<close>
  161.15 +ML_file \<open>Tools/cartprod.ML\<close>
  161.16 +ML_file \<open>Tools/inductive_package.ML\<close>
  161.17 +ML_file \<open>Tools/induct_tacs.ML\<close>
  161.18 +ML_file \<open>Tools/primrec_package.ML\<close>
  161.19  
  161.20  ML \<open>
  161.21  structure Lfp =
   162.1 --- a/src/ZF/pair.thy	Sun Jan 06 13:44:33 2019 +0100
   162.2 +++ b/src/ZF/pair.thy	Sun Jan 06 15:04:34 2019 +0100
   162.3 @@ -8,7 +8,7 @@
   162.4  theory pair imports upair
   162.5  begin
   162.6  
   162.7 -ML_file "simpdata.ML"
   162.8 +ML_file \<open>simpdata.ML\<close>
   162.9  
  162.10  setup \<open>
  162.11    map_theory_simpset
   163.1 --- a/src/ZF/upair.thy	Sun Jan 06 13:44:33 2019 +0100
   163.2 +++ b/src/ZF/upair.thy	Sun Jan 06 15:04:34 2019 +0100
   163.3 @@ -16,7 +16,7 @@
   163.4  keywords "print_tcset" :: diag
   163.5  begin
   163.6  
   163.7 -ML_file "Tools/typechk.ML"
   163.8 +ML_file \<open>Tools/typechk.ML\<close>
   163.9  
  163.10  lemma atomize_ball [symmetric, rulify]:
  163.11       "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"