--- a/etc/options Sun Jan 06 12:32:01 2019 +0100
+++ b/etc/options Sun Jan 06 15:11:13 2019 +0100
@@ -288,6 +288,9 @@
option update_control_cartouches : bool = false
-- "update antiquotations to use control symbol with cartouche argument"
+option update_path_cartouches : bool = false
+ -- "update file-system paths to use cartouches"
+
section "Build Database"
--- a/src/CTT/CTT.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/CTT/CTT.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
section \<open>Constructive Type Theory: axiomatic basis\<close>
-ML_file "~~/src/Provers/typedsimp.ML"
+ML_file \<open>~~/src/Provers/typedsimp.ML\<close>
setup Pure_Thy.old_appl_syntax_setup
typedecl i
@@ -455,7 +455,7 @@
method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close>
method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close>
-ML_file "rew.ML"
+ML_file \<open>rew.ML\<close>
method_setup rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))\<close>
method_setup hyp_rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))\<close>
--- a/src/Doc/Classes/Setup.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Classes/Setup.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2,8 +2,8 @@
imports Main
begin
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
declare [[default_code_width = 74]]
--- a/src/Doc/Codegen/Introduction.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Codegen/Introduction.thy Sun Jan 06 15:11:13 2019 +0100
@@ -69,7 +69,7 @@
text \<open>\noindent Then we can generate code e.g.~for \<open>SML\<close> as follows:\<close>
export_code %quote empty dequeue enqueue in SML
- module_name Example file "$ISABELLE_TMP/example.ML"
+ module_name Example file \<open>$ISABELLE_TMP/example.ML\<close>
text \<open>\noindent resulting in the following code:\<close>
@@ -90,7 +90,7 @@
\<close>
export_code %quote empty dequeue enqueue in Haskell
- module_name Example file "$ISABELLE_TMP/examples/"
+ module_name Example file \<open>$ISABELLE_TMP/examples/\<close>
text \<open>
\noindent This is the corresponding code:
--- a/src/Doc/Codegen/Setup.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Codegen/Setup.thy Sun Jan 06 15:11:13 2019 +0100
@@ -7,8 +7,8 @@
"HOL-Library.IArray"
begin
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
no_syntax (output)
"_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3)
--- a/src/Doc/Datatypes/Setup.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Datatypes/Setup.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2,6 +2,6 @@
imports Main
begin
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
end
--- a/src/Doc/Eisbach/Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Eisbach/Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -6,7 +6,7 @@
imports Main
begin
-ML_file "~~/src/Doc/antiquote_setup.ML"
+ML_file \<open>~~/src/Doc/antiquote_setup.ML\<close>
ML\<open>
fun get_split_rule ctxt target =
--- a/src/Doc/Implementation/Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Implementation/Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
imports Main
begin
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
end
--- a/src/Doc/Isar_Ref/Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Isar_Ref/Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
imports Pure
begin
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
end
--- a/src/Doc/JEdit/Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/JEdit/Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
imports Main
begin
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
end
--- a/src/Doc/Logics_ZF/ZF_Isar.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy Sun Jan 06 15:11:13 2019 +0100
@@ -3,7 +3,7 @@
begin
(*<*)
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
(*>*)
chapter \<open>Some Isar language elements\<close>
--- a/src/Doc/System/Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/System/Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
imports Pure
begin
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
end
--- a/src/Doc/System/Sessions.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/System/Sessions.thy Sun Jan 06 15:11:13 2019 +0100
@@ -734,16 +734,18 @@
example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by
``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.)
+ \<^item> @{system_option update_path_cartouches} to update file-system paths to
+ use cartouches: this depends on language markup provided by semantic
+ processing of parsed input.
+
It is also possible to produce custom updates in Isabelle/ML, by reporting
\<^ML>\<open>Markup.update\<close> with the precise source position and a replacement
text. This operation should be made conditional on specific system options,
similar to the ones above. Searching the above option names in ML sources of
\<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples.
- Different update options can be in conflict by producing overlapping edits:
- this may require to run @{tool update} multiple times, but it is often
- better to enable particular update options separately and commit the changes
- one-by-one.
+ Updates can be in conflict by producing nested or overlapping edits: this
+ may require to run @{tool update} multiple times.
\<close>
@@ -769,7 +771,7 @@
separately with special options as follows:
@{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
- -o record_proofs=2 -o parallel_proofs=0\<close>}
+ -o record_proofs=2\<close>}
\<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing
Isabelle/ML heap sizes for very big PIDE processes that include many
--- a/src/Doc/Tutorial/Inductive/Advanced.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Inductive/Advanced.thy Sun Jan 06 15:11:13 2019 +0100
@@ -1,5 +1,5 @@
(*<*)theory Advanced imports Even begin
-ML_file "../../antiquote_setup.ML"
+ML_file \<open>../../antiquote_setup.ML\<close>
(*>*)
text \<open>
--- a/src/Doc/Tutorial/Inductive/Even.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Inductive/Even.thy Sun Jan 06 15:11:13 2019 +0100
@@ -1,5 +1,5 @@
(*<*)theory Even imports Main begin
-ML_file "../../antiquote_setup.ML"
+ML_file \<open>../../antiquote_setup.ML\<close>
(*>*)
section\<open>The Set of Even Numbers\<close>
--- a/src/Doc/Tutorial/Protocol/Message.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
section\<open>Theory of Agents and Messages for Security Protocols\<close>
theory Message imports Main begin
-ML_file "../../antiquote_setup.ML"
+ML_file \<open>../../antiquote_setup.ML\<close>
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
--- a/src/Doc/Tutorial/Types/Setup.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Types/Setup.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2,7 +2,7 @@
imports Main
begin
-ML_file "../../antiquote_setup.ML"
-ML_file "../../more_antiquote.ML"
+ML_file \<open>../../antiquote_setup.ML\<close>
+ML_file \<open>../../more_antiquote.ML\<close>
end
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2,8 +2,8 @@
imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
begin
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
attribute_setup all =
\<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
--- a/src/FOL/FOL.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOL/FOL.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,9 +9,9 @@
keywords "print_claset" "print_induct_rules" :: diag
begin
-ML_file "~~/src/Provers/classical.ML"
-ML_file "~~/src/Provers/blast.ML"
-ML_file "~~/src/Provers/clasimp.ML"
+ML_file \<open>~~/src/Provers/classical.ML\<close>
+ML_file \<open>~~/src/Provers/blast.ML\<close>
+ML_file \<open>~~/src/Provers/clasimp.ML\<close>
subsection \<open>The classical axiom\<close>
@@ -335,7 +335,7 @@
not_imp not_all not_ex cases_simp cla_simps_misc
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close>
simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close>
@@ -361,7 +361,7 @@
Simplifier.method_setup Splitter.split_modifiers
\<close>
-ML_file "~~/src/Tools/eqsubst.ML"
+ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
subsection \<open>Other simple lemmas\<close>
@@ -429,7 +429,7 @@
text \<open>Method setup.\<close>
-ML_file "~~/src/Tools/induct.ML"
+ML_file \<open>~~/src/Tools/induct.ML\<close>
ML \<open>
structure Induct = Induct
(
@@ -447,7 +447,7 @@
end
-ML_file "~~/src/Tools/case_product.ML"
+ML_file \<open>~~/src/Tools/case_product.ML\<close>
hide_const (open) eq
--- a/src/FOL/IFOL.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOL/IFOL.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,16 +9,16 @@
begin
ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
-ML_file "~~/src/Tools/misc_legacy.ML"
-ML_file "~~/src/Provers/splitter.ML"
-ML_file "~~/src/Provers/hypsubst.ML"
-ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
-ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
-ML_file "~~/src/Provers/quantifier1.ML"
-ML_file "~~/src/Tools/intuitionistic.ML"
-ML_file "~~/src/Tools/project_rule.ML"
-ML_file "~~/src/Tools/atomize_elim.ML"
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
+ML_file \<open>~~/src/Provers/splitter.ML\<close>
+ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
+ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
+ML_file \<open>~~/src/Tools/intuitionistic.ML\<close>
+ML_file \<open>~~/src/Tools/project_rule.ML\<close>
+ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
subsection \<open>Syntax and axiomatic basis\<close>
@@ -582,7 +582,7 @@
)
\<close>
-ML_file "fologic.ML"
+ML_file \<open>fologic.ML\<close>
lemma thin_refl: \<open>\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W\<close> .
@@ -603,7 +603,7 @@
open Hypsubst;
\<close>
-ML_file "intprover.ML"
+ML_file \<open>intprover.ML\<close>
subsection \<open>Intuitionistic Reasoning\<close>
--- a/src/FOLP/FOLP.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOLP/FOLP.thy Sun Jan 06 15:11:13 2019 +0100
@@ -98,8 +98,8 @@
apply assumption
done
-ML_file "classical.ML" (* Patched because matching won't instantiate proof *)
-ML_file "simp.ML" (* Patched because matching won't instantiate proof *)
+ML_file \<open>classical.ML\<close> (* Patched because matching won't instantiate proof *)
+ML_file \<open>simp.ML\<close> (* Patched because matching won't instantiate proof *)
ML \<open>
structure Cla = Classical
@@ -138,6 +138,6 @@
apply (tactic \<open>ALLGOALS (Cla.fast_tac \<^context> FOLP_cs)\<close>)
done
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
end
--- a/src/FOLP/IFOLP.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOLP/IFOLP.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
imports Pure
begin
-ML_file "~~/src/Tools/misc_legacy.ML"
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
setup Pure_Thy.old_appl_syntax_setup
@@ -605,7 +605,7 @@
lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
-ML_file "hypsubst.ML"
+ML_file \<open>hypsubst.ML\<close>
ML \<open>
structure Hypsubst = Hypsubst
@@ -627,7 +627,7 @@
open Hypsubst;
\<close>
-ML_file "intprover.ML"
+ML_file \<open>intprover.ML\<close>
(*** Rewrite rules ***)
--- a/src/HOL/ATP.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/ATP.thy Sun Jan 06 15:11:13 2019 +0100
@@ -11,11 +11,11 @@
subsection \<open>ATP problems and proofs\<close>
-ML_file "Tools/ATP/atp_util.ML"
-ML_file "Tools/ATP/atp_problem.ML"
-ML_file "Tools/ATP/atp_proof.ML"
-ML_file "Tools/ATP/atp_proof_redirect.ML"
-ML_file "Tools/ATP/atp_satallax.ML"
+ML_file \<open>Tools/ATP/atp_util.ML\<close>
+ML_file \<open>Tools/ATP/atp_problem.ML\<close>
+ML_file \<open>Tools/ATP/atp_proof.ML\<close>
+ML_file \<open>Tools/ATP/atp_proof_redirect.ML\<close>
+ML_file \<open>Tools/ATP/atp_satallax.ML\<close>
subsection \<open>Higher-order reasoning helpers\<close>
@@ -146,12 +146,12 @@
subsection \<open>Basic connection between ATPs and HOL\<close>
-ML_file "Tools/lambda_lifting.ML"
-ML_file "Tools/monomorph.ML"
-ML_file "Tools/ATP/atp_problem_generate.ML"
-ML_file "Tools/ATP/atp_proof_reconstruct.ML"
-ML_file "Tools/ATP/atp_systems.ML"
-ML_file "Tools/ATP/atp_waldmeister.ML"
+ML_file \<open>Tools/lambda_lifting.ML\<close>
+ML_file \<open>Tools/monomorph.ML\<close>
+ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
+ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
+ML_file \<open>Tools/ATP/atp_waldmeister.ML\<close>
hide_fact (open) waldmeister_fol boolean_equality boolean_comm
--- a/src/HOL/Algebra/Ring.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Algebra/Ring.thy Sun Jan 06 15:11:13 2019 +0100
@@ -418,7 +418,7 @@
compute distributive normal form in locale contexts\<close>
-ML_file "ringsimp.ML"
+ML_file \<open>ringsimp.ML\<close>
attribute_setup algebra = \<open>
Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
--- a/src/HOL/Analysis/Measurable.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Analysis/Measurable.thy Sun Jan 06 15:11:13 2019 +0100
@@ -46,7 +46,7 @@
lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
-ML_file "measurable.ML"
+ML_file \<open>measurable.ML\<close>
attribute_setup measurable = \<open>
Scan.lift (
--- a/src/HOL/Analysis/Norm_Arith.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy Sun Jan 06 15:11:13 2019 +0100
@@ -129,7 +129,7 @@
mult_1_left
mult_1_right
-ML_file "normarith.ML"
+ML_file \<open>normarith.ML\<close>
method_setup%important norm = \<open>
Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
--- a/src/HOL/Argo.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Argo.thy Sun Jan 06 15:11:13 2019 +0100
@@ -6,22 +6,22 @@
imports HOL
begin
-ML_file "~~/src/Tools/Argo/argo_expr.ML"
-ML_file "~~/src/Tools/Argo/argo_term.ML"
-ML_file "~~/src/Tools/Argo/argo_lit.ML"
-ML_file "~~/src/Tools/Argo/argo_proof.ML"
-ML_file "~~/src/Tools/Argo/argo_rewr.ML"
-ML_file "~~/src/Tools/Argo/argo_cls.ML"
-ML_file "~~/src/Tools/Argo/argo_common.ML"
-ML_file "~~/src/Tools/Argo/argo_cc.ML"
-ML_file "~~/src/Tools/Argo/argo_simplex.ML"
-ML_file "~~/src/Tools/Argo/argo_thy.ML"
-ML_file "~~/src/Tools/Argo/argo_heap.ML"
-ML_file "~~/src/Tools/Argo/argo_cdcl.ML"
-ML_file "~~/src/Tools/Argo/argo_core.ML"
-ML_file "~~/src/Tools/Argo/argo_clausify.ML"
-ML_file "~~/src/Tools/Argo/argo_solver.ML"
+ML_file \<open>~~/src/Tools/Argo/argo_expr.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_term.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_lit.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_proof.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_rewr.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cls.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_common.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cc.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_simplex.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_thy.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_heap.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cdcl.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_core.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_clausify.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_solver.ML\<close>
-ML_file "Tools/Argo/argo_tactic.ML"
+ML_file \<open>Tools/Argo/argo_tactic.ML\<close>
end
--- a/src/HOL/BNF_Composition.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Composition.thy Sun Jan 06 15:11:13 2019 +0100
@@ -178,9 +178,9 @@
lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
unfolding id_bnf_def by unfold_locales auto
-ML_file "Tools/BNF/bnf_comp_tactics.ML"
-ML_file "Tools/BNF/bnf_comp.ML"
-ML_file "Tools/BNF/bnf_lift.ML"
+ML_file \<open>Tools/BNF/bnf_comp_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_comp.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lift.ML\<close>
hide_fact
DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0
--- a/src/HOL/BNF_Def.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Def.thy Sun Jan 06 15:11:13 2019 +0100
@@ -272,9 +272,9 @@
lemma eq_onp_mono_iff: "eq_onp P \<le> eq_onp Q \<longleftrightarrow> P \<le> Q"
unfolding eq_onp_def by auto
-ML_file "Tools/BNF/bnf_util.ML"
-ML_file "Tools/BNF/bnf_tactics.ML"
-ML_file "Tools/BNF/bnf_def_tactics.ML"
-ML_file "Tools/BNF/bnf_def.ML"
+ML_file \<open>Tools/BNF/bnf_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_def_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_def.ML\<close>
end
--- a/src/HOL/BNF_Fixpoint_Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -287,12 +287,12 @@
lemma Let_const: "Let x (\<lambda>_. c) = c"
unfolding Let_def ..
-ML_file "Tools/BNF/bnf_fp_util_tactics.ML"
-ML_file "Tools/BNF/bnf_fp_util.ML"
-ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
-ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
-ML_file "Tools/BNF/bnf_fp_n2m.ML"
-ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
+ML_file \<open>Tools/BNF/bnf_fp_util_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_def_sugar_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_def_sugar.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_n2m_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_n2m.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_n2m_sugar.ML\<close>
end
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Sun Jan 06 15:11:13 2019 +0100
@@ -281,10 +281,10 @@
thus "univ f X \<in> B" using x PRES by simp
qed
-ML_file "Tools/BNF/bnf_gfp_util.ML"
-ML_file "Tools/BNF/bnf_gfp_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
+ML_file \<open>Tools/BNF/bnf_gfp_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar.ML\<close>
end
--- a/src/HOL/BNF_Least_Fixpoint.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy Sun Jan 06 15:11:13 2019 +0100
@@ -196,11 +196,11 @@
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)"
unfolding fun.pred_map unfolding comp_def id_def ..
-ML_file "Tools/BNF/bnf_lfp_util.ML"
-ML_file "Tools/BNF/bnf_lfp_tactics.ML"
-ML_file "Tools/BNF/bnf_lfp.ML"
-ML_file "Tools/BNF/bnf_lfp_compat.ML"
-ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
-ML_file "Tools/BNF/bnf_lfp_size.ML"
+ML_file \<open>Tools/BNF/bnf_lfp_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_compat.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar_more.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_size.ML\<close>
end
--- a/src/HOL/Basic_BNF_LFPs.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Basic_BNF_LFPs.thy Sun Jan 06 15:11:13 2019 +0100
@@ -102,7 +102,7 @@
lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))"
by (force simp: rel_prod.simps elim: rel_prod.cases)
-ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
+ML_file \<open>Tools/BNF/bnf_lfp_basic_sugar.ML\<close>
declare prod.size [no_atp]
--- a/src/HOL/Code_Evaluation.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Code_Evaluation.thy Sun Jan 06 15:11:13 2019 +0100
@@ -94,11 +94,11 @@
| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
-ML_file "Tools/code_evaluation.ML"
+ML_file \<open>Tools/code_evaluation.ML\<close>
code_reserved Eval Code_Evaluation
-ML_file "~~/src/HOL/Tools/value_command.ML"
+ML_file \<open>~~/src/HOL/Tools/value_command.ML\<close>
subsection \<open>Dedicated \<open>term_of\<close> instances\<close>
@@ -141,7 +141,7 @@
subsection \<open>Generic reification\<close>
-ML_file "~~/src/HOL/Tools/reification.ML"
+ML_file \<open>~~/src/HOL/Tools/reification.ML\<close>
subsection \<open>Diagnostic\<close>
--- a/src/HOL/Ctr_Sugar.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Ctr_Sugar.thy Sun Jan 06 15:11:13 2019 +0100
@@ -27,7 +27,7 @@
declare [[coercion_args case_abs -]]
declare [[coercion_args case_elem - +]]
-ML_file "Tools/Ctr_Sugar/case_translation.ML"
+ML_file \<open>Tools/Ctr_Sugar/case_translation.ML\<close>
lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
by (erule iffI) (erule contrapos_pn)
@@ -37,13 +37,13 @@
"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
by blast+
-ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
-ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
-ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
-ML_file "Tools/Ctr_Sugar/ctr_sugar.ML"
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_util.ML\<close>
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_tactics.ML\<close>
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_code.ML\<close>
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar.ML\<close>
text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close>
-ML_file "Tools/coinduction.ML"
+ML_file \<open>Tools/coinduction.ML\<close>
end
--- a/src/HOL/Decision_Procs/Approximation.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Jan 06 15:11:13 2019 +0100
@@ -1635,7 +1635,7 @@
"n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
by (simp_all add: real_div_nat_eq_floor_of_divide minus_div_mult_eq_mod [symmetric])
-ML_file "approximation.ML"
+ML_file \<open>approximation.ML\<close>
method_setup approximation = \<open>
let
@@ -1667,7 +1667,7 @@
"\<not> \<not> q \<longleftrightarrow> q"
by auto
-ML_file "approximation_generator.ML"
+ML_file \<open>approximation_generator.ML\<close>
setup "Approximation_Generator.setup"
end
--- a/src/HOL/Decision_Procs/Cooper.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2527,7 +2527,7 @@
end
\<close>
-ML_file "cooper_tac.ML"
+ML_file \<open>cooper_tac.ML\<close>
method_setup cooper = \<open>
Scan.lift (Args.mode "no_quantify") >>
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,8 +9,8 @@
imports Main
begin
-ML_file "langford_data.ML"
-ML_file "ferrante_rackoff_data.ML"
+ML_file \<open>langford_data.ML\<close>
+ML_file \<open>ferrante_rackoff_data.ML\<close>
context linorder
begin
@@ -424,7 +424,7 @@
lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
-ML_file "langford.ML"
+ML_file \<open>langford.ML\<close>
method_setup dlo = \<open>
Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
\<close> "Langford's algorithm for quantifier elimination in dense linear orders"
@@ -746,7 +746,7 @@
end
-ML_file "ferrante_rackoff.ML"
+ML_file \<open>ferrante_rackoff.ML\<close>
method_setup ferrack = \<open>
Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
--- a/src/HOL/Decision_Procs/Ferrack.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2546,7 +2546,7 @@
end
\<close>
-ML_file "ferrack_tac.ML"
+ML_file \<open>ferrack_tac.ML\<close>
method_setup rferrack = \<open>
Scan.lift (Args.mode "no_quantify") >>
--- a/src/HOL/Decision_Procs/MIR.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Sun Jan 06 15:11:13 2019 +0100
@@ -5696,7 +5696,7 @@
of_int_less_iff [where 'a = real, symmetric]
of_int_le_iff [where 'a = real, symmetric]
-ML_file "mir_tac.ML"
+ML_file \<open>mir_tac.ML\<close>
method_setup mir = \<open>
Scan.lift (Args.mode "no_quantify") >>
--- a/src/HOL/Eisbach/Eisbach.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Eisbach/Eisbach.thy Sun Jan 06 15:11:13 2019 +0100
@@ -15,10 +15,10 @@
"uses"
begin
-ML_file "parse_tools.ML"
-ML_file "method_closure.ML"
-ML_file "eisbach_rule_insts.ML"
-ML_file "match_method.ML"
+ML_file \<open>parse_tools.ML\<close>
+ML_file \<open>method_closure.ML\<close>
+ML_file \<open>eisbach_rule_insts.ML\<close>
+ML_file \<open>match_method.ML\<close>
method solves methods m = (m; fail)
--- a/src/HOL/Extraction.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Extraction.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Option
begin
-ML_file "Tools/rewrite_hol_proof.ML"
+ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
subsection \<open>Setup\<close>
--- a/src/HOL/Fields.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fields.thy Sun Jan 06 15:11:13 2019 +0100
@@ -57,8 +57,8 @@
text \<open>Setup for linear arithmetic prover\<close>
-ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
-ML_file "Tools/lin_arith.ML"
+ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
+ML_file \<open>Tools/lin_arith.ML\<close>
setup \<open>Lin_Arith.global_setup\<close>
declaration \<open>K Lin_Arith.setup\<close>
--- a/src/HOL/Fun.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fun.thy Sun Jan 06 15:11:13 2019 +0100
@@ -886,7 +886,7 @@
subsubsection \<open>Functorial structure of types\<close>
-ML_file "Tools/functor.ML"
+ML_file \<open>Tools/functor.ML\<close>
functor map_fun: map_fun
by (simp_all add: fun_eq_iff)
--- a/src/HOL/Fun_Def.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fun_Def.thy Sun Jan 06 15:11:13 2019 +0100
@@ -77,25 +77,25 @@
lemma wf_in_rel: "wf R \<Longrightarrow> wfP (in_rel R)"
by (simp add: wfP_def)
-ML_file "Tools/Function/function_core.ML"
-ML_file "Tools/Function/mutual.ML"
-ML_file "Tools/Function/pattern_split.ML"
-ML_file "Tools/Function/relation.ML"
-ML_file "Tools/Function/function_elims.ML"
+ML_file \<open>Tools/Function/function_core.ML\<close>
+ML_file \<open>Tools/Function/mutual.ML\<close>
+ML_file \<open>Tools/Function/pattern_split.ML\<close>
+ML_file \<open>Tools/Function/relation.ML\<close>
+ML_file \<open>Tools/Function/function_elims.ML\<close>
method_setup relation = \<open>
Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
\<close> "prove termination using a user-specified wellfounded relation"
-ML_file "Tools/Function/function.ML"
-ML_file "Tools/Function/pat_completeness.ML"
+ML_file \<open>Tools/Function/function.ML\<close>
+ML_file \<open>Tools/Function/pat_completeness.ML\<close>
method_setup pat_completeness = \<open>
Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
\<close> "prove completeness of (co)datatype patterns"
-ML_file "Tools/Function/fun.ML"
-ML_file "Tools/Function/induction_schema.ML"
+ML_file \<open>Tools/Function/fun.ML\<close>
+ML_file \<open>Tools/Function/induction_schema.ML\<close>
method_setup induction_schema = \<open>
Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
@@ -108,7 +108,7 @@
where is_measure_trivial: "is_measure f"
named_theorems measure_function "rules that guide the heuristic generation of measure functions"
-ML_file "Tools/Function/measure_functions.ML"
+ML_file \<open>Tools/Function/measure_functions.ML\<close>
lemma measure_size[measure_function]: "is_measure size"
by (rule is_measure_trivial)
@@ -119,7 +119,7 @@
lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
by (rule is_measure_trivial)
-ML_file "Tools/Function/lexicographic_order.ML"
+ML_file \<open>Tools/Function/lexicographic_order.ML\<close>
method_setup lexicographic_order = \<open>
Method.sections clasimp_modifiers >>
@@ -290,10 +290,10 @@
subsection \<open>Tool setup\<close>
-ML_file "Tools/Function/termination.ML"
-ML_file "Tools/Function/scnp_solve.ML"
-ML_file "Tools/Function/scnp_reconstruct.ML"
-ML_file "Tools/Function/fun_cases.ML"
+ML_file \<open>Tools/Function/termination.ML\<close>
+ML_file \<open>Tools/Function/scnp_solve.ML\<close>
+ML_file \<open>Tools/Function/scnp_reconstruct.ML\<close>
+ML_file \<open>Tools/Function/fun_cases.ML\<close>
ML_val \<comment> \<open>setup inactive\<close>
\<open>
--- a/src/HOL/Fun_Def_Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fun_Def_Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,15 +8,15 @@
imports Ctr_Sugar Set Wellfounded
begin
-ML_file "Tools/Function/function_lib.ML"
+ML_file \<open>Tools/Function/function_lib.ML\<close>
named_theorems termination_simp "simplification rules for termination proofs"
-ML_file "Tools/Function/function_common.ML"
-ML_file "Tools/Function/function_context_tree.ML"
+ML_file \<open>Tools/Function/function_common.ML\<close>
+ML_file \<open>Tools/Function/function_context_tree.ML\<close>
attribute_setup fundef_cong =
\<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close>
"declaration of congruence rule for function definitions"
-ML_file "Tools/Function/sum_tree.ML"
+ML_file \<open>Tools/Function/sum_tree.ML\<close>
end
--- a/src/HOL/Groebner_Basis.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Groebner_Basis.thy Sun Jan 06 15:11:13 2019 +0100
@@ -33,7 +33,7 @@
by auto
named_theorems algebra "pre-simplification rules for algebraic methods"
-ML_file "Tools/groebner.ML"
+ML_file \<open>Tools/groebner.ML\<close>
method_setup algebra = \<open>
let
--- a/src/HOL/Groups.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Groups.thy Sun Jan 06 15:11:13 2019 +0100
@@ -988,7 +988,7 @@
end
-ML_file "Tools/group_cancel.ML"
+ML_file \<open>Tools/group_cancel.ML\<close>
simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
\<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
--- a/src/HOL/HOL.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOL.thy Sun Jan 06 15:11:13 2019 +0100
@@ -12,26 +12,26 @@
"quickcheck_params" :: thy_decl
begin
-ML_file "~~/src/Tools/misc_legacy.ML"
-ML_file "~~/src/Tools/try.ML"
-ML_file "~~/src/Tools/quickcheck.ML"
-ML_file "~~/src/Tools/solve_direct.ML"
-ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
-ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
-ML_file "~~/src/Provers/hypsubst.ML"
-ML_file "~~/src/Provers/splitter.ML"
-ML_file "~~/src/Provers/classical.ML"
-ML_file "~~/src/Provers/blast.ML"
-ML_file "~~/src/Provers/clasimp.ML"
-ML_file "~~/src/Tools/eqsubst.ML"
-ML_file "~~/src/Provers/quantifier1.ML"
-ML_file "~~/src/Tools/atomize_elim.ML"
-ML_file "~~/src/Tools/cong_tac.ML"
-ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
-ML_file "~~/src/Tools/project_rule.ML"
-ML_file "~~/src/Tools/subtyping.ML"
-ML_file "~~/src/Tools/case_product.ML"
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
+ML_file \<open>~~/src/Tools/try.ML\<close>
+ML_file \<open>~~/src/Tools/quickcheck.ML\<close>
+ML_file \<open>~~/src/Tools/solve_direct.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
+ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
+ML_file \<open>~~/src/Provers/splitter.ML\<close>
+ML_file \<open>~~/src/Provers/classical.ML\<close>
+ML_file \<open>~~/src/Provers/blast.ML\<close>
+ML_file \<open>~~/src/Provers/clasimp.ML\<close>
+ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
+ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
+ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
+ML_file \<open>~~/src/Tools/cong_tac.ML\<close>
+ML_file \<open>~~/src/Tools/intuitionistic.ML\<close> setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
+ML_file \<open>~~/src/Tools/project_rule.ML\<close>
+ML_file \<open>~~/src/Tools/subtyping.ML\<close>
+ML_file \<open>~~/src/Tools/case_product.ML\<close>
ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
@@ -776,7 +776,7 @@
subsection \<open>Package setup\<close>
-ML_file "Tools/hologic.ML"
+ML_file \<open>Tools/hologic.ML\<close>
subsubsection \<open>Sledgehammer setup\<close>
@@ -1202,7 +1202,7 @@
lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
by blast
-ML_file "Tools/simpdata.ML"
+ML_file \<open>Tools/simpdata.ML\<close>
ML \<open>open Simpdata\<close>
setup \<open>
@@ -1484,7 +1484,7 @@
text \<open>Method setup.\<close>
-ML_file "~~/src/Tools/induct.ML"
+ML_file \<open>~~/src/Tools/induct.ML\<close>
ML \<open>
structure Induct = Induct
(
@@ -1499,7 +1499,7 @@
)
\<close>
-ML_file "~~/src/Tools/induction.ML"
+ML_file \<open>~~/src/Tools/induction.ML\<close>
declaration \<open>
fn _ => Induct.map_simpset (fn ss => ss
@@ -1584,12 +1584,12 @@
end
-ML_file "~~/src/Tools/induct_tacs.ML"
+ML_file \<open>~~/src/Tools/induct_tacs.ML\<close>
subsubsection \<open>Coherent logic\<close>
-ML_file "~~/src/Tools/coherent.ML"
+ML_file \<open>~~/src/Tools/coherent.ML\<close>
ML \<open>
structure Coherent = Coherent
(
@@ -1735,7 +1735,7 @@
val trans = @{thm trans}
\<close>
-ML_file "Tools/cnf.ML"
+ML_file \<open>Tools/cnf.ML\<close>
section \<open>\<open>NO_MATCH\<close> simproc\<close>
--- a/src/HOL/HOLCF/Cpodef.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy Sun Jan 06 15:11:13 2019 +0100
@@ -279,6 +279,6 @@
subsection \<open>HOLCF type definition package\<close>
-ML_file "Tools/cpodef.ML"
+ML_file \<open>Tools/cpodef.ML\<close>
end
--- a/src/HOL/HOLCF/Domain.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Domain.thy Sun Jan 06 15:11:13 2019 +0100
@@ -150,7 +150,7 @@
(\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>)]
\<close>
-ML_file "Tools/domaindef.ML"
+ML_file \<open>Tools/domaindef.ML\<close>
subsection \<open>Isomorphic deflations\<close>
@@ -319,9 +319,9 @@
named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
-ML_file "Tools/Domain/domain_isomorphism.ML"
-ML_file "Tools/Domain/domain_axioms.ML"
-ML_file "Tools/Domain/domain.ML"
+ML_file \<open>Tools/Domain/domain_isomorphism.ML\<close>
+ML_file \<open>Tools/Domain/domain_axioms.ML\<close>
+ML_file \<open>Tools/Domain/domain.ML\<close>
lemmas [domain_defl_simps] =
DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
--- a/src/HOL/HOLCF/Domain_Aux.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy Sun Jan 06 15:11:13 2019 +0100
@@ -355,10 +355,10 @@
named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
and domain_map_ID "theorems like foo_map$ID = ID"
-ML_file "Tools/Domain/domain_take_proofs.ML"
-ML_file "Tools/cont_consts.ML"
-ML_file "Tools/cont_proc.ML"
-ML_file "Tools/Domain/domain_constructors.ML"
-ML_file "Tools/Domain/domain_induction.ML"
+ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close>
+ML_file \<open>Tools/cont_consts.ML\<close>
+ML_file \<open>Tools/cont_proc.ML\<close>
+ML_file \<open>Tools/Domain/domain_constructors.ML\<close>
+ML_file \<open>Tools/Domain/domain_induction.ML\<close>
end
--- a/src/HOL/HOLCF/Fixrec.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy Sun Jan 06 15:11:13 2019 +0100
@@ -224,8 +224,8 @@
subsection \<open>Initializing the fixrec package\<close>
-ML_file "Tools/holcf_library.ML"
-ML_file "Tools/fixrec.ML"
+ML_file \<open>Tools/holcf_library.ML\<close>
+ML_file \<open>Tools/fixrec.ML\<close>
method_setup fixrec_simp = \<open>
Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports IOA.IOA Env Impl Impl_finite
begin
-ML_file "Check.ML"
+ML_file \<open>Check.ML\<close>
primrec reduce :: "'a list => 'a list"
where
--- a/src/HOL/Hilbert_Choice.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sun Jan 06 15:11:13 2019 +0100
@@ -903,7 +903,7 @@
lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c"
by (simp only: someI_ex)
-ML_file "Tools/choice_specification.ML"
+ML_file \<open>Tools/choice_specification.ML\<close>
subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close>
--- a/src/HOL/Hoare/Hoare_Logic.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Sun Jan 06 15:11:13 2019 +0100
@@ -53,7 +53,7 @@
"_hoare" :: "['a assn,'a com,'a assn] => bool"
("{_} // _ // {_}" [0,55,0] 50)
-ML_file "hoare_syntax.ML"
+ML_file \<open>hoare_syntax.ML\<close>
parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
@@ -93,7 +93,7 @@
by blast
lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
-ML_file "hoare_tac.ML"
+ML_file \<open>hoare_tac.ML\<close>
method_setup vcg = \<open>
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Sun Jan 06 15:11:13 2019 +0100
@@ -55,7 +55,7 @@
"_hoare_abort" :: "['a assn,'a com,'a assn] => bool"
("{_} // _ // {_}" [0,55,0] 50)
-ML_file "hoare_syntax.ML"
+ML_file \<open>hoare_syntax.ML\<close>
parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
print_translation
\<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
@@ -104,7 +104,7 @@
lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
by blast
-ML_file "hoare_tac.ML"
+ML_file \<open>hoare_tac.ML\<close>
method_setup vcg = \<open>
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
--- a/src/HOL/Import/Import_Setup.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Import/Import_Setup.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
begin
-ML_file "import_data.ML"
+ML_file \<open>import_data.ML\<close>
lemma light_ex_imp_nonempty:
"P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
@@ -26,7 +26,7 @@
"(\<And>x. f x = g x) \<Longrightarrow> f = g"
by auto
-ML_file "import_rule.ML"
+ML_file \<open>import_rule.ML\<close>
end
--- a/src/HOL/Inductive.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Inductive.thy Sun Jan 06 15:11:13 2019 +0100
@@ -413,7 +413,7 @@
lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
by auto
-ML_file "Tools/inductive.ML"
+ML_file \<open>Tools/inductive.ML\<close>
lemmas [mono] =
imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
@@ -514,14 +514,14 @@
text \<open>Package setup.\<close>
-ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
-ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
-ML_file "Tools/Old_Datatype/old_datatype_data.ML"
-ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
-ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
-ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
-ML_file "Tools/Old_Datatype/old_primrec.ML"
-ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
+ML_file \<open>Tools/Old_Datatype/old_datatype_aux.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_datatype_prop.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_datatype_data.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_rep_datatype.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_datatype_codegen.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_util.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_primrec.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar.ML\<close>
text \<open>Lambda-abstractions with pattern matching:\<close>
syntax (ASCII)
--- a/src/HOL/Int.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Int.thy Sun Jan 06 15:11:13 2019 +0100
@@ -1081,7 +1081,7 @@
lemmas of_int_simps =
of_int_0 of_int_1 of_int_add of_int_mult
-ML_file "Tools/int_arith.ML"
+ML_file \<open>Tools/int_arith.ML\<close>
declaration \<open>K Int_Arith.setup\<close>
simproc_setup fast_arith
--- a/src/HOL/Isar_Examples/Hoare.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Sun Jan 06 15:11:13 2019 +0100
@@ -401,7 +401,7 @@
lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
-ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
+ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
method_setup hoare =
\<open>Scan.succeed (fn ctxt =>
--- a/src/HOL/Lattices.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Lattices.thy Sun Jan 06 15:11:13 2019 +0100
@@ -693,7 +693,7 @@
end
-ML_file "Tools/boolean_algebra_cancel.ML"
+ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
\<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
--- a/src/HOL/Library/Adhoc_Overloading.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Adhoc_Overloading.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,6 +10,6 @@
keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl
begin
-ML_file "adhoc_overloading.ML"
+ML_file \<open>adhoc_overloading.ML\<close>
end
--- a/src/HOL/Library/BNF_Axiomatization.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/BNF_Axiomatization.thy Sun Jan 06 15:11:13 2019 +0100
@@ -13,6 +13,6 @@
"bnf_axiomatization" :: thy_decl
begin
-ML_file "../Tools/BNF/bnf_axiomatization.ML"
+ML_file \<open>../Tools/BNF/bnf_axiomatization.ML\<close>
end
--- a/src/HOL/Library/BNF_Corec.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/BNF_Corec.thy Sun Jan 06 15:11:13 2019 +0100
@@ -201,12 +201,12 @@
named_theorems friend_of_corec_simps
-ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_tactics.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_util.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_unique_sugar.ML\<close>
method_setup transfer_prover_eq = \<open>
Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
--- a/src/HOL/Library/Cancellation.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Cancellation.thy Sun Jan 06 15:11:13 2019 +0100
@@ -76,9 +76,9 @@
subsection \<open>Simproc Set-Up\<close>
-ML_file "Cancellation/cancel.ML"
-ML_file "Cancellation/cancel_data.ML"
-ML_file "Cancellation/cancel_simprocs.ML"
+ML_file \<open>Cancellation/cancel.ML\<close>
+ML_file \<open>Cancellation/cancel_data.ML\<close>
+ML_file \<open>Cancellation/cancel_simprocs.ML\<close>
end
--- a/src/HOL/Library/Case_Converter.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Case_Converter.thy Sun Jan 06 15:11:13 2019 +0100
@@ -18,6 +18,6 @@
"missing_pattern_match = Code.abort"
unfolding missing_pattern_match_def Code.abort_def ..
-ML_file "case_converter.ML"
+ML_file \<open>case_converter.ML\<close>
end
--- a/src/HOL/Library/Code_Lazy.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Code_Lazy.thy Sun Jan 06 15:11:13 2019 +0100
@@ -227,7 +227,7 @@
subsection \<open>Implementation\<close>
-ML_file "code_lazy.ML"
+ML_file \<open>code_lazy.ML\<close>
setup \<open>
Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
--- a/src/HOL/Library/Code_Prolog.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Code_Prolog.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
keywords "values_prolog" :: diag
begin
-ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+ML_file \<open>~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML\<close>
section \<open>Setup for Numerals\<close>
--- a/src/HOL/Library/Code_Test.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Code_Test.thy Sun Jan 06 15:11:13 2019 +0100
@@ -142,6 +142,6 @@
subsection \<open>Test engine and drivers\<close>
-ML_file "code_test.ML"
+ML_file \<open>code_test.ML\<close>
end
--- a/src/HOL/Library/Conditional_Parametricity.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Conditional_Parametricity.thy Sun Jan 06 15:11:13 2019 +0100
@@ -43,6 +43,6 @@
end
-ML_file "conditional_parametricity.ML"
+ML_file \<open>conditional_parametricity.ML\<close>
end
--- a/src/HOL/Library/Countable.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Countable.thy Sun Jan 06 15:11:13 2019 +0100
@@ -200,7 +200,7 @@
subsection \<open>Automatically proving countability of datatypes\<close>
-ML_file "../Tools/BNF/bnf_lfp_countable.ML"
+ML_file \<open>../Tools/BNF/bnf_lfp_countable.ML\<close>
ML \<open>
fun countable_datatype_tac ctxt st =
--- a/src/HOL/Library/Datatype_Records.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Datatype_Records.thy Sun Jan 06 15:11:13 2019 +0100
@@ -82,7 +82,7 @@
named_theorems datatype_record_update
-ML_file "datatype_records.ML"
+ML_file \<open>datatype_records.ML\<close>
setup \<open>Datatype_Records.setup\<close>
end
\ No newline at end of file
--- a/src/HOL/Library/Multiset.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Jan 06 15:11:13 2019 +0100
@@ -969,7 +969,7 @@
unfolding subset_mset_def repeat_mset_iterate_add
by (simp add: iterate_add_eq_add_iff2 mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add])
-ML_file "multiset_simprocs.ML"
+ML_file \<open>multiset_simprocs.ML\<close>
lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close>
by simp
--- a/src/HOL/Library/Old_Datatype.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Old_Datatype.thy Sun Jan 06 15:11:13 2019 +0100
@@ -508,6 +508,6 @@
hide_type (open) node item
hide_const (open) Push Node Atom Leaf Numb Lim Split Case
-ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
+ML_file \<open>~~/src/HOL/Tools/Old_Datatype/old_datatype.ML\<close>
end
--- a/src/HOL/Library/Old_Recdef.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Old_Recdef.thy Sun Jan 06 15:11:13 2019 +0100
@@ -57,7 +57,7 @@
lemma tfl_exE: "\<exists>x. P x \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q \<Longrightarrow> Q"
by blast
-ML_file "old_recdef.ML"
+ML_file \<open>old_recdef.ML\<close>
subsection \<open>Rule setup\<close>
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,6 +8,6 @@
imports Predicate_Compile_Alternative_Defs
begin
-ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
+ML_file \<open>../Tools/Predicate_Compile/predicate_compile_quickcheck.ML\<close>
end
--- a/src/HOL/Library/Realizers.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Realizers.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Main
begin
-ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
-ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
+ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close>
+ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close>
end
--- a/src/HOL/Library/Reflection.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Reflection.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Main
begin
-ML_file "~~/src/HOL/Tools/reflection.ML"
+ML_file \<open>~~/src/HOL/Tools/reflection.ML\<close>
method_setup reify = \<open>
Attrib.thms --
--- a/src/HOL/Library/Refute.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Refute.thy Sun Jan 06 15:11:13 2019 +0100
@@ -14,7 +14,7 @@
"refute_params" :: thy_decl
begin
-ML_file "refute.ML"
+ML_file \<open>refute.ML\<close>
refute_params
[itself = 1,
--- a/src/HOL/Library/Rewrite.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Rewrite.thy Sun Jan 06 15:11:13 2019 +0100
@@ -30,7 +30,7 @@
apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
done
-ML_file "cconv.ML"
-ML_file "rewrite.ML"
+ML_file \<open>cconv.ML\<close>
+ML_file \<open>rewrite.ML\<close>
end
--- a/src/HOL/Library/Simps_Case_Conv.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Simps_Case_Conv.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,6 +8,6 @@
abbrevs "simps_of_case" "case_of_simps" = ""
begin
-ML_file "simps_case_conv.ML"
+ML_file \<open>simps_case_conv.ML\<close>
end
--- a/src/HOL/Library/Sum_of_Squares.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Sum_of_Squares.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,9 +10,9 @@
imports Complex_Main
begin
-ML_file "positivstellensatz.ML"
-ML_file "Sum_of_Squares/sum_of_squares.ML"
-ML_file "Sum_of_Squares/positivstellensatz_tools.ML"
-ML_file "Sum_of_Squares/sos_wrapper.ML"
+ML_file \<open>positivstellensatz.ML\<close>
+ML_file \<open>Sum_of_Squares/sum_of_squares.ML\<close>
+ML_file \<open>Sum_of_Squares/positivstellensatz_tools.ML\<close>
+ML_file \<open>Sum_of_Squares/sos_wrapper.ML\<close>
end
--- a/src/HOL/Lifting.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Lifting.thy Sun Jan 06 15:11:13 2019 +0100
@@ -552,22 +552,22 @@
subsection \<open>ML setup\<close>
-ML_file "Tools/Lifting/lifting_util.ML"
+ML_file \<open>Tools/Lifting/lifting_util.ML\<close>
named_theorems relator_eq_onp
"theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
-ML_file "Tools/Lifting/lifting_info.ML"
+ML_file \<open>Tools/Lifting/lifting_info.ML\<close>
(* setup for the function type *)
declare fun_quotient[quot_map]
declare fun_mono[relator_mono]
lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
-ML_file "Tools/Lifting/lifting_bnf.ML"
-ML_file "Tools/Lifting/lifting_term.ML"
-ML_file "Tools/Lifting/lifting_def.ML"
-ML_file "Tools/Lifting/lifting_setup.ML"
-ML_file "Tools/Lifting/lifting_def_code_dt.ML"
+ML_file \<open>Tools/Lifting/lifting_bnf.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_term.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_def.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_setup.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_def_code_dt.ML\<close>
lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
by(cases xy) simp
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Complex_Main "HOL-Library.Lattice_Algebras"
begin
-ML_file "~~/src/Tools/float.ML"
+ML_file \<open>~~/src/Tools/float.ML\<close>
(*FIXME surely floor should be used? This file is full of redundant material.*)
@@ -235,6 +235,6 @@
lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
-ML_file "float_arith.ML"
+ML_file \<open>float_arith.ML\<close>
end
--- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Sun Jan 06 15:11:13 2019 +0100
@@ -7,13 +7,13 @@
theory Compute_Oracle imports HOL.HOL
begin
-ML_file "am.ML"
-ML_file "am_compiler.ML"
-ML_file "am_interpreter.ML"
-ML_file "am_ghc.ML"
-ML_file "am_sml.ML"
-ML_file "report.ML"
-ML_file "compute.ML"
-ML_file "linker.ML"
+ML_file \<open>am.ML\<close>
+ML_file \<open>am_compiler.ML\<close>
+ML_file \<open>am_interpreter.ML\<close>
+ML_file \<open>am_ghc.ML\<close>
+ML_file \<open>am_sml.ML\<close>
+ML_file \<open>report.ML\<close>
+ML_file \<open>compute.ML\<close>
+ML_file \<open>linker.ML\<close>
end
--- a/src/HOL/Matrix_LP/Cplex.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Matrix_LP/Cplex.thy Sun Jan 06 15:11:13 2019 +0100
@@ -6,10 +6,10 @@
imports SparseMatrix LP ComputeFloat ComputeNumeral
begin
-ML_file "Cplex_tools.ML"
-ML_file "CplexMatrixConverter.ML"
-ML_file "FloatSparseMatrixBuilder.ML"
-ML_file "fspmlp.ML"
+ML_file \<open>Cplex_tools.ML\<close>
+ML_file \<open>CplexMatrixConverter.ML\<close>
+ML_file \<open>FloatSparseMatrixBuilder.ML\<close>
+ML_file \<open>fspmlp.ML\<close>
lemma spm_mult_le_dual_prts:
assumes
@@ -64,7 +64,7 @@
(mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
-ML_file "matrixlp.ML"
+ML_file \<open>matrixlp.ML\<close>
end
--- a/src/HOL/Meson.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Meson.thy Sun Jan 06 15:11:13 2019 +0100
@@ -195,9 +195,9 @@
subsection \<open>Meson package\<close>
-ML_file "Tools/Meson/meson.ML"
-ML_file "Tools/Meson/meson_clausify.ML"
-ML_file "Tools/Meson/meson_tactic.ML"
+ML_file \<open>Tools/Meson/meson.ML\<close>
+ML_file \<open>Tools/Meson/meson_clausify.ML\<close>
+ML_file \<open>Tools/Meson/meson_tactic.ML\<close>
hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
--- a/src/HOL/Metis.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Metis.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
imports ATP
begin
-ML_file "~~/src/Tools/Metis/metis.ML"
+ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
subsection \<open>Literal selection and lambda-lifting helpers\<close>
@@ -38,9 +38,9 @@
subsection \<open>Metis package\<close>
-ML_file "Tools/Metis/metis_generate.ML"
-ML_file "Tools/Metis/metis_reconstruct.ML"
-ML_file "Tools/Metis/metis_tactic.ML"
+ML_file \<open>Tools/Metis/metis_generate.ML\<close>
+ML_file \<open>Tools/Metis/metis_reconstruct.ML\<close>
+ML_file \<open>Tools/Metis/metis_tactic.ML\<close>
hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
--- a/src/HOL/Mirabelle/Mirabelle.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Mirabelle/Mirabelle.thy Sun Jan 06 15:11:13 2019 +0100
@@ -6,8 +6,8 @@
imports Main
begin
-ML_file "Tools/mirabelle.ML"
-ML_file "../TPTP/sledgehammer_tactics.ML"
+ML_file \<open>Tools/mirabelle.ML\<close>
+ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close>
ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close>
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,13 +8,13 @@
imports Main Mirabelle
begin
-ML_file "Tools/mirabelle_arith.ML"
-ML_file "Tools/mirabelle_metis.ML"
-ML_file "Tools/mirabelle_quickcheck.ML"
-ML_file "Tools/mirabelle_refute.ML"
-ML_file "Tools/mirabelle_sledgehammer.ML"
-ML_file "Tools/mirabelle_sledgehammer_filter.ML"
-ML_file "Tools/mirabelle_try0.ML"
+ML_file \<open>Tools/mirabelle_arith.ML\<close>
+ML_file \<open>Tools/mirabelle_metis.ML\<close>
+ML_file \<open>Tools/mirabelle_quickcheck.ML\<close>
+ML_file \<open>Tools/mirabelle_refute.ML\<close>
+ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close>
+ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close>
+ML_file \<open>Tools/mirabelle_try0.ML\<close>
text \<open>
Only perform type-checking of the actions,
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Sun Jan 06 15:11:13 2019 +0100
@@ -11,8 +11,8 @@
"~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
begin
-ML_file "mutabelle.ML"
-ML_file "mutabelle_extra.ML"
+ML_file \<open>mutabelle.ML\<close>
+ML_file \<open>mutabelle_extra.ML\<close>
section \<open>configuration\<close>
--- a/src/HOL/Nat.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nat.thy Sun Jan 06 15:11:13 2019 +0100
@@ -1930,7 +1930,7 @@
shows "u = s"
using assms(2,1) by (rule trans)
-ML_file "Tools/nat_arith.ML"
+ML_file \<open>Tools/nat_arith.ML\<close>
simproc_setup nateq_cancel_sums
("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
--- a/src/HOL/Nitpick.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nitpick.thy Sun Jan 06 15:11:13 2019 +0100
@@ -201,21 +201,21 @@
definition wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
"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"
-ML_file "Tools/Nitpick/kodkod.ML"
-ML_file "Tools/Nitpick/kodkod_sat.ML"
-ML_file "Tools/Nitpick/nitpick_util.ML"
-ML_file "Tools/Nitpick/nitpick_hol.ML"
-ML_file "Tools/Nitpick/nitpick_mono.ML"
-ML_file "Tools/Nitpick/nitpick_preproc.ML"
-ML_file "Tools/Nitpick/nitpick_scope.ML"
-ML_file "Tools/Nitpick/nitpick_peephole.ML"
-ML_file "Tools/Nitpick/nitpick_rep.ML"
-ML_file "Tools/Nitpick/nitpick_nut.ML"
-ML_file "Tools/Nitpick/nitpick_kodkod.ML"
-ML_file "Tools/Nitpick/nitpick_model.ML"
-ML_file "Tools/Nitpick/nitpick.ML"
-ML_file "Tools/Nitpick/nitpick_commands.ML"
-ML_file "Tools/Nitpick/nitpick_tests.ML"
+ML_file \<open>Tools/Nitpick/kodkod.ML\<close>
+ML_file \<open>Tools/Nitpick/kodkod_sat.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_util.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_hol.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_mono.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_preproc.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_scope.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_peephole.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_rep.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_nut.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_kodkod.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_model.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_commands.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_tests.ML\<close>
setup \<open>
Nitpick_HOL.register_ersatz_global
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Sun Jan 06 15:11:13 2019 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-ML_file "minipick.ML"
+ML_file \<open>minipick.ML\<close>
nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
total_consts = smart]
--- a/src/HOL/Nominal/Nominal.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nominal/Nominal.thy Sun Jan 06 15:11:13 2019 +0100
@@ -3561,7 +3561,7 @@
(*******************************************************)
(* Setup of the theorem attributes eqvt and eqvt_force *)
-ML_file "nominal_thmdecls.ML"
+ML_file \<open>nominal_thmdecls.ML\<close>
setup "NominalThmDecls.setup"
lemmas [eqvt] =
@@ -3597,11 +3597,11 @@
(***************************************)
(* setup for the individial atom-kinds *)
(* and nominal datatypes *)
-ML_file "nominal_atoms.ML"
+ML_file \<open>nominal_atoms.ML\<close>
(************************************************************)
(* various tactics for analysing permutations, supports etc *)
-ML_file "nominal_permeq.ML"
+ML_file \<open>nominal_permeq.ML\<close>
method_setup perm_simp =
\<open>NominalPermeq.perm_simp_meth\<close>
@@ -3645,7 +3645,7 @@
(*****************************************************************)
(* tactics for generating fresh names and simplifying fresh_funs *)
-ML_file "nominal_fresh_fun.ML"
+ML_file \<open>nominal_fresh_fun.ML\<close>
method_setup generate_fresh = \<open>
Args.type_name {proper = true, strict = true} >>
@@ -3663,20 +3663,20 @@
lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
using assms ..
-ML_file "nominal_datatype.ML"
+ML_file \<open>nominal_datatype.ML\<close>
(******************************************************)
(* primitive recursive functions on nominal datatypes *)
-ML_file "nominal_primrec.ML"
+ML_file \<open>nominal_primrec.ML\<close>
(****************************************************)
(* inductive definition involving nominal datatypes *)
-ML_file "nominal_inductive.ML"
-ML_file "nominal_inductive2.ML"
+ML_file \<open>nominal_inductive.ML\<close>
+ML_file \<open>nominal_inductive2.ML\<close>
(*****************************************)
(* setup for induction principles method *)
-ML_file "nominal_induct.ML"
+ML_file \<open>nominal_induct.ML\<close>
method_setup nominal_induct =
\<open>NominalInduct.nominal_induct_method\<close>
\<open>nominal induction\<close>
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Jan 06 15:11:13 2019 +0100
@@ -99,7 +99,7 @@
where "star_of x \<equiv> star_n (\<lambda>n. x)"
text \<open>Initialize transfer tactic.\<close>
-ML_file "transfer_principle.ML"
+ML_file \<open>transfer_principle.ML\<close>
method_setup transfer =
\<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))\<close>
--- a/src/HOL/Num.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Num.thy Sun Jan 06 15:11:13 2019 +0100
@@ -292,7 +292,7 @@
syntax
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
-ML_file "Tools/numeral.ML"
+ML_file \<open>Tools/numeral.ML\<close>
parse_translation \<open>
let
--- a/src/HOL/Numeral_Simprocs.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Sun Jan 06 15:11:13 2019 +0100
@@ -6,11 +6,11 @@
imports Divides
begin
-ML_file "~~/src/Provers/Arith/assoc_fold.ML"
-ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
-ML_file "~~/src/Provers/Arith/combine_numerals.ML"
-ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
-ML_file "~~/src/Provers/Arith/extract_common_term.ML"
+ML_file \<open>~~/src/Provers/Arith/assoc_fold.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/cancel_numeral_factor.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/extract_common_term.ML\<close>
lemmas semiring_norm =
Let_def arith_simps diff_nat_numeral rel_simps
@@ -103,7 +103,7 @@
fixes x:: "'a::comm_ring_1" shows "numeral w * -x = x * - numeral w"
by (simp add: mult.commute)
-ML_file "Tools/numeral_simprocs.ML"
+ML_file \<open>Tools/numeral_simprocs.ML\<close>
simproc_setup semiring_assoc_fold
("(a::'a::comm_semiring_1_cancel) * b") =
@@ -213,7 +213,7 @@
|"(l::'a::field) / (m * n)") =
\<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>
-ML_file "Tools/nat_numeral_simprocs.ML"
+ML_file \<open>Tools/nat_numeral_simprocs.ML\<close>
simproc_setup nat_combine_numerals
("(i::nat) + j" | "Suc (i + j)") =
--- a/src/HOL/Nunchaku.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nunchaku.thy Sun Jan 06 15:11:13 2019 +0100
@@ -29,16 +29,16 @@
definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
"rmember A x \<longleftrightarrow> x \<in> A"
-ML_file "Tools/Nunchaku/nunchaku_util.ML"
-ML_file "Tools/Nunchaku/nunchaku_collect.ML"
-ML_file "Tools/Nunchaku/nunchaku_problem.ML"
-ML_file "Tools/Nunchaku/nunchaku_translate.ML"
-ML_file "Tools/Nunchaku/nunchaku_model.ML"
-ML_file "Tools/Nunchaku/nunchaku_reconstruct.ML"
-ML_file "Tools/Nunchaku/nunchaku_display.ML"
-ML_file "Tools/Nunchaku/nunchaku_tool.ML"
-ML_file "Tools/Nunchaku/nunchaku.ML"
-ML_file "Tools/Nunchaku/nunchaku_commands.ML"
+ML_file \<open>Tools/Nunchaku/nunchaku_util.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_collect.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_problem.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_translate.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_model.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_reconstruct.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_display.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_tool.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_commands.ML\<close>
hide_const (open) unreachable The_unsafe rmember
--- a/src/HOL/Orderings.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Orderings.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,8 +9,8 @@
keywords "print_orders" :: diag
begin
-ML_file "~~/src/Provers/order.ML"
-ML_file "~~/src/Provers/quasi.ML" (* FIXME unused? *)
+ML_file \<open>~~/src/Provers/order.ML\<close>
+ML_file \<open>~~/src/Provers/quasi.ML\<close> (* FIXME unused? *)
subsection \<open>Abstract ordering\<close>
--- a/src/HOL/Partial_Function.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Partial_Function.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
begin
named_theorems partial_function_mono "monotonicity rules for partial function definitions"
-ML_file "Tools/Function/partial_function.ML"
+ML_file \<open>Tools/Function/partial_function.ML\<close>
lemma (in ccpo) in_chain_finite:
assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}"
--- a/src/HOL/Predicate_Compile.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Predicate_Compile.thy Sun Jan 06 15:11:13 2019 +0100
@@ -11,17 +11,17 @@
"values" :: diag
begin
-ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML"
-ML_file "Tools/Predicate_Compile/core_data.ML"
-ML_file "Tools/Predicate_Compile/mode_inference.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_core.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_data.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile.ML"
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_aux.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_compilations.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/core_data.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/mode_inference.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_proof.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_core.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_data.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_fun.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_pred.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_specialisation.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile.ML\<close>
subsection \<open>Set membership as a generator predicate\<close>
--- a/src/HOL/Presburger.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Presburger.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,8 +9,8 @@
keywords "try0" :: diag
begin
-ML_file "Tools/Qelim/qelim.ML"
-ML_file "Tools/Qelim/cooper_procedure.ML"
+ML_file \<open>Tools/Qelim/qelim.ML\<close>
+ML_file \<open>Tools/Qelim/cooper_procedure.ML\<close>
subsection\<open>The \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Properties\<close>
@@ -390,7 +390,7 @@
"\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<and> P) = (0 \<le> x' \<and> P')"
by (simp cong: conj_cong)
-ML_file "Tools/Qelim/cooper.ML"
+ML_file \<open>Tools/Qelim/cooper.ML\<close>
method_setup presburger = \<open>
let
@@ -505,6 +505,6 @@
subsection \<open>Try0\<close>
-ML_file "Tools/try0.ML"
+ML_file \<open>Tools/try0.ML\<close>
end
--- a/src/HOL/Product_Type.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Product_Type.thy Sun Jan 06 15:11:13 2019 +0100
@@ -738,7 +738,7 @@
lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
by (simp only: internal_case_prod_def case_prod_conv)
-ML_file "Tools/split_rule.ML"
+ML_file \<open>Tools/split_rule.ML\<close>
hide_const internal_case_prod
@@ -1263,7 +1263,7 @@
subsection \<open>Simproc for rewriting a set comprehension into a pointfree expression\<close>
-ML_file "Tools/set_comprehension_pointfree.ML"
+ML_file \<open>Tools/set_comprehension_pointfree.ML\<close>
setup \<open>
Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
@@ -1309,7 +1309,7 @@
| _ => NONE)
\<close>
-ML_file "Tools/inductive_set.ML"
+ML_file \<open>Tools/inductive_set.ML\<close>
subsection \<open>Legacy theorem bindings and duplicates\<close>
--- a/src/HOL/Prolog/HOHH.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Prolog/HOHH.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports HOL.HOL
begin
-ML_file "prolog.ML"
+ML_file \<open>prolog.ML\<close>
method_setup ptac =
\<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Sun Jan 06 15:11:13 2019 +0100
@@ -206,7 +206,7 @@
@{thm [display] pigeonhole_slow_def}
The program for searching for an element in an array is
@{thm [display,eta_contract=false] search_def}
- The correctness statement for @{term "pigeonhole"} is
+ The correctness statement for \<^term>\<open>pigeonhole\<close> is
@{thm [display] pigeonhole_correctness [no_vars]}
In order to analyze the speed of the above programs,
--- a/src/HOL/Quickcheck_Exhaustive.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Jan 06 15:11:13 2019 +0100
@@ -705,14 +705,14 @@
notation (output) unknown ("?")
-ML_file "Tools/Quickcheck/exhaustive_generators.ML"
+ML_file \<open>Tools/Quickcheck/exhaustive_generators.ML\<close>
declare [[quickcheck_batch_tester = exhaustive]]
subsection \<open>Defining generators for abstract types\<close>
-ML_file "Tools/Quickcheck/abstract_generators.ML"
+ML_file \<open>Tools/Quickcheck/abstract_generators.ML\<close>
hide_fact (open) orelse_def
no_notation orelse (infixr "orelse" 55)
--- a/src/HOL/Quickcheck_Narrowing.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Sun Jan 06 15:11:13 2019 +0100
@@ -192,9 +192,9 @@
subsubsection \<open>Setting up the counterexample generator\<close>
-external_file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
-external_file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
-ML_file "Tools/Quickcheck/narrowing_generators.ML"
+external_file \<open>~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\<close>
+external_file \<open>~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\<close>
+ML_file \<open>Tools/Quickcheck/narrowing_generators.ML\<close>
definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
where
@@ -318,7 +318,7 @@
subsection \<open>The \<open>find_unused_assms\<close> command\<close>
-ML_file "Tools/Quickcheck/find_unused_assms.ML"
+ML_file \<open>Tools/Quickcheck/find_unused_assms.ML\<close>
subsection \<open>Closing up\<close>
--- a/src/HOL/Quickcheck_Random.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quickcheck_Random.thy Sun Jan 06 15:11:13 2019 +0100
@@ -209,8 +209,8 @@
subsection \<open>Deriving random generators for datatypes\<close>
-ML_file "Tools/Quickcheck/quickcheck_common.ML"
-ML_file "Tools/Quickcheck/random_generators.ML"
+ML_file \<open>Tools/Quickcheck/quickcheck_common.ML\<close>
+ML_file \<open>Tools/Quickcheck/random_generators.ML\<close>
subsection \<open>Code setup\<close>
--- a/src/HOL/Quotient.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quotient.thy Sun Jan 06 15:11:13 2019 +0100
@@ -636,7 +636,7 @@
and quot_preserve "preservation theorems"
and id_simps "identity simp rules for maps"
and quot_thm "quotient theorems"
-ML_file "Tools/Quotient/quotient_info.ML"
+ML_file \<open>Tools/Quotient/quotient_info.ML\<close>
declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
@@ -657,15 +657,15 @@
vimage_id
text \<open>Translation functions for the lifting process.\<close>
-ML_file "Tools/Quotient/quotient_term.ML"
+ML_file \<open>Tools/Quotient/quotient_term.ML\<close>
text \<open>Definitions of the quotient types.\<close>
-ML_file "Tools/Quotient/quotient_type.ML"
+ML_file \<open>Tools/Quotient/quotient_type.ML\<close>
text \<open>Definitions for quotient constants.\<close>
-ML_file "Tools/Quotient/quotient_def.ML"
+ML_file \<open>Tools/Quotient/quotient_def.ML\<close>
text \<open>
@@ -692,7 +692,7 @@
begin
text \<open>Tactics for proving the lifted theorems\<close>
-ML_file "Tools/Quotient/quotient_tacs.ML"
+ML_file \<open>Tools/Quotient/quotient_tacs.ML\<close>
end
--- a/src/HOL/Real.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Real.thy Sun Jan 06 15:11:13 2019 +0100
@@ -1644,8 +1644,8 @@
subsection \<open>Setup for SMT\<close>
-ML_file "Tools/SMT/smt_real.ML"
-ML_file "Tools/SMT/z3_real.ML"
+ML_file \<open>Tools/SMT/smt_real.ML\<close>
+ML_file \<open>Tools/SMT/z3_real.ML\<close>
lemma [z3_rule]:
"0 + x = x"
@@ -1660,6 +1660,6 @@
subsection \<open>Setup for Argo\<close>
-ML_file "Tools/Argo/argo_real.ML"
+ML_file \<open>Tools/Argo/argo_real.ML\<close>
end
--- a/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy Sun Jan 06 15:11:13 2019 +0100
@@ -3,7 +3,7 @@
imports "HOL-Real_Asymp.Real_Asymp"
begin
-ML_file "~~/src/Doc/antiquote_setup.ML"
+ML_file \<open>~~/src/Doc/antiquote_setup.ML\<close>
(*>*)
section \<open>Introduction\<close>
--- a/src/HOL/Record.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Record.thy Sun Jan 06 15:11:13 2019 +0100
@@ -453,7 +453,7 @@
subsection \<open>Record package\<close>
-ML_file "Tools/record.ML"
+ML_file \<open>Tools/record.ML\<close>
hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
--- a/src/HOL/Rings.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Rings.thy Sun Jan 06 15:11:13 2019 +0100
@@ -1762,9 +1762,9 @@
text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
named_theorems arith "arith facts -- only ground formulas"
-ML_file "Tools/arith_data.ML"
-
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+ML_file \<open>Tools/arith_data.ML\<close>
+
+ML_file \<open>~~/src/Provers/Arith/cancel_div_mod.ML\<close>
ML \<open>
structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
--- a/src/HOL/SAT.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SAT.thy Sun Jan 06 15:11:13 2019 +0100
@@ -11,10 +11,10 @@
imports Argo
begin
-ML_file "Tools/prop_logic.ML"
-ML_file "Tools/sat_solver.ML"
-ML_file "Tools/sat.ML"
-ML_file "Tools/Argo/argo_sat_solver.ML"
+ML_file \<open>Tools/prop_logic.ML\<close>
+ML_file \<open>Tools/sat_solver.ML\<close>
+ML_file \<open>Tools/sat.ML\<close>
+ML_file \<open>Tools/Argo/argo_sat_solver.ML\<close>
method_setup sat = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\<close>
"SAT solver"
--- a/src/HOL/SMT.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SMT.thy Sun Jan 06 15:11:13 2019 +0100
@@ -286,35 +286,35 @@
subsection \<open>Setup\<close>
-ML_file "Tools/SMT/smt_util.ML"
-ML_file "Tools/SMT/smt_failure.ML"
-ML_file "Tools/SMT/smt_config.ML"
-ML_file "Tools/SMT/smt_builtin.ML"
-ML_file "Tools/SMT/smt_datatypes.ML"
-ML_file "Tools/SMT/smt_normalize.ML"
-ML_file "Tools/SMT/smt_translate.ML"
-ML_file "Tools/SMT/smtlib.ML"
-ML_file "Tools/SMT/smtlib_interface.ML"
-ML_file "Tools/SMT/smtlib_proof.ML"
-ML_file "Tools/SMT/smtlib_isar.ML"
-ML_file "Tools/SMT/z3_proof.ML"
-ML_file "Tools/SMT/z3_isar.ML"
-ML_file "Tools/SMT/smt_solver.ML"
-ML_file "Tools/SMT/cvc4_interface.ML"
-ML_file "Tools/SMT/cvc4_proof_parse.ML"
-ML_file "Tools/SMT/verit_proof.ML"
-ML_file "Tools/SMT/verit_isar.ML"
-ML_file "Tools/SMT/verit_proof_parse.ML"
-ML_file "Tools/SMT/conj_disj_perm.ML"
-ML_file "Tools/SMT/smt_replay_methods.ML"
-ML_file "Tools/SMT/smt_replay.ML"
-ML_file "Tools/SMT/z3_interface.ML"
-ML_file "Tools/SMT/z3_replay_rules.ML"
-ML_file "Tools/SMT/z3_replay_methods.ML"
-ML_file "Tools/SMT/z3_replay.ML"
-ML_file "Tools/SMT/verit_replay_methods.ML"
-ML_file "Tools/SMT/verit_replay.ML"
-ML_file "Tools/SMT/smt_systems.ML"
+ML_file \<open>Tools/SMT/smt_util.ML\<close>
+ML_file \<open>Tools/SMT/smt_failure.ML\<close>
+ML_file \<open>Tools/SMT/smt_config.ML\<close>
+ML_file \<open>Tools/SMT/smt_builtin.ML\<close>
+ML_file \<open>Tools/SMT/smt_datatypes.ML\<close>
+ML_file \<open>Tools/SMT/smt_normalize.ML\<close>
+ML_file \<open>Tools/SMT/smt_translate.ML\<close>
+ML_file \<open>Tools/SMT/smtlib.ML\<close>
+ML_file \<open>Tools/SMT/smtlib_interface.ML\<close>
+ML_file \<open>Tools/SMT/smtlib_proof.ML\<close>
+ML_file \<open>Tools/SMT/smtlib_isar.ML\<close>
+ML_file \<open>Tools/SMT/z3_proof.ML\<close>
+ML_file \<open>Tools/SMT/z3_isar.ML\<close>
+ML_file \<open>Tools/SMT/smt_solver.ML\<close>
+ML_file \<open>Tools/SMT/cvc4_interface.ML\<close>
+ML_file \<open>Tools/SMT/cvc4_proof_parse.ML\<close>
+ML_file \<open>Tools/SMT/verit_proof.ML\<close>
+ML_file \<open>Tools/SMT/verit_isar.ML\<close>
+ML_file \<open>Tools/SMT/verit_proof_parse.ML\<close>
+ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close>
+ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/smt_replay.ML\<close>
+ML_file \<open>Tools/SMT/z3_interface.ML\<close>
+ML_file \<open>Tools/SMT/z3_replay_rules.ML\<close>
+ML_file \<open>Tools/SMT/z3_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/z3_replay.ML\<close>
+ML_file \<open>Tools/SMT/verit_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/verit_replay.ML\<close>
+ML_file \<open>Tools/SMT/smt_systems.ML\<close>
method_setup smt = \<open>
Scan.optional Attrib.thms [] >>
--- a/src/HOL/SMT_Examples/Boogie.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SMT_Examples/Boogie.thy Sun Jan 06 15:11:13 2019 +0100
@@ -45,7 +45,7 @@
section \<open>Setup\<close>
-ML_file "boogie.ML"
+ML_file \<open>boogie.ML\<close>
@@ -55,22 +55,22 @@
declare [[smt_read_only_certificates = true]]
-external_file "Boogie_Max.certs"
+external_file \<open>Boogie_Max.certs\<close>
declare [[smt_certificates = "Boogie_Max.certs"]]
-boogie_file Boogie_Max
+boogie_file \<open>Boogie_Max\<close>
-external_file "Boogie_Dijkstra.certs"
+external_file \<open>Boogie_Dijkstra.certs\<close>
declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
-boogie_file Boogie_Dijkstra
+boogie_file \<open>Boogie_Dijkstra\<close>
declare [[z3_extensions = true]]
-external_file "VCC_Max.certs"
+external_file \<open>VCC_Max.certs\<close>
declare [[smt_certificates = "VCC_Max.certs"]]
-boogie_file VCC_Max
+boogie_file \<open>VCC_Max\<close>
end
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Complex_Main
begin
-external_file "SMT_Examples.certs"
+external_file \<open>SMT_Examples.certs\<close>
declare [[smt_certificates = "SMT_Examples.certs"]]
declare [[smt_read_only_certificates = true]]
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
spark_proof_functions
gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
-spark_open "greatest_common_divisor/g_c_d"
+spark_open \<open>greatest_common_divisor/g_c_d\<close>
spark_vc procedure_g_c_d_4
proof -
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Sun Jan 06 15:11:13 2019 +0100
@@ -541,7 +541,7 @@
text \<open>The verification conditions\<close>
-spark_open "liseq/liseq_length"
+spark_open \<open>liseq/liseq_length\<close>
spark_vc procedure_liseq_length_5
by (simp_all add: liseq_singleton liseq'_singleton)
--- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification
begin
-spark_open "rmd/f"
+spark_open \<open>rmd/f\<close>
spark_vc function_f_2
using assms by simp_all
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification
begin
-spark_open "rmd/hash"
+spark_open \<open>rmd/hash\<close>
abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
"from_chain c \<equiv> (
--- a/src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification
begin
-spark_open "rmd/k_l"
+spark_open \<open>rmd/k_l\<close>
spark_vc function_k_l_6
using assms by (simp add: K_def)
--- a/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification
begin
-spark_open "rmd/k_r"
+spark_open \<open>rmd/k_r\<close>
spark_vc function_k_r_6
using assms by (simp add: K'_def)
--- a/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification RMD_Lemmas
begin
-spark_open "rmd/r_l"
+spark_open \<open>rmd/r_l\<close>
spark_vc function_r_l_2
proof -
--- a/src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification RMD_Lemmas
begin
-spark_open "rmd/r_r"
+spark_open \<open>rmd/r_r\<close>
spark_vc function_r_r_2
proof -
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification
begin
-spark_open "rmd/round"
+spark_open \<open>rmd/round\<close>
abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
"from_chain c \<equiv> (
--- a/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification RMD_Lemmas
begin
-spark_open "rmd/s_l"
+spark_open \<open>rmd/s_l\<close>
spark_vc function_s_l_2
proof -
--- a/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports RMD_Specification RMD_Lemmas
begin
-spark_open "rmd/s_r"
+spark_open \<open>rmd/s_r\<close>
spark_vc function_s_r_2
proof -
--- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Sun Jan 06 15:11:13 2019 +0100
@@ -7,7 +7,7 @@
imports "HOL-SPARK.SPARK"
begin
-spark_open "sqrt/isqrt"
+spark_open \<open>sqrt/isqrt\<close>
spark_vc function_isqrt_4
proof -
--- a/src/HOL/SPARK/Manual/Complex_Types.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Complex_Types.thy Sun Jan 06 15:11:13 2019 +0100
@@ -31,7 +31,7 @@
complex_types__initialized3 = initialized3
(*<*)
-spark_open "complex_types_app/initialize"
+spark_open \<open>complex_types_app/initialize\<close>
spark_vc procedure_initialize_1
by (simp add: initialized_def)
--- a/src/HOL/SPARK/Manual/Proc1.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Proc1.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2,7 +2,7 @@
imports "HOL-SPARK.SPARK"
begin
-spark_open "loop_invariant/proc1"
+spark_open \<open>loop_invariant/proc1\<close>
spark_vc procedure_proc1_5
by (simp add: ring_distribs mod_simps)
--- a/src/HOL/SPARK/Manual/Proc2.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Proc2.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2,7 +2,7 @@
imports "HOL-SPARK.SPARK"
begin
-spark_open "loop_invariant/proc2"
+spark_open \<open>loop_invariant/proc2\<close>
spark_vc procedure_proc2_7
by (simp add: ring_distribs mod_simps)
--- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
spark_proof_functions
gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
-spark_open "simple_greatest_common_divisor/g_c_d"
+spark_open \<open>simple_greatest_common_divisor/g_c_d\<close>
spark_vc procedure_g_c_d_4
using \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>
--- a/src/HOL/SPARK/SPARK_Setup.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy Sun Jan 06 15:11:13 2019 +0100
@@ -15,8 +15,8 @@
"spark_status" :: diag
begin
-ML_file "Tools/fdl_lexer.ML"
-ML_file "Tools/fdl_parser.ML"
+ML_file \<open>Tools/fdl_lexer.ML\<close>
+ML_file \<open>Tools/fdl_parser.ML\<close>
text \<open>
SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
@@ -181,7 +181,7 @@
text \<open>Load the package\<close>
-ML_file "Tools/spark_vcs.ML"
-ML_file "Tools/spark_commands.ML"
+ML_file \<open>Tools/spark_vcs.ML\<close>
+ML_file \<open>Tools/spark_commands.ML\<close>
end
--- a/src/HOL/Semiring_Normalization.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Semiring_Normalization.thy Sun Jan 06 15:11:13 2019 +0100
@@ -67,7 +67,7 @@
text \<open>Semiring normalization proper\<close>
-ML_file "Tools/semiring_normalizer.ML"
+ML_file \<open>Tools/semiring_normalizer.ML\<close>
context comm_semiring_1
begin
--- a/src/HOL/Sledgehammer.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Sledgehammer.thy Sun Jan 06 15:11:13 2019 +0100
@@ -16,23 +16,23 @@
lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
by (erule contrapos_nn) (rule arg_cong)
-ML_file "Tools/Sledgehammer/async_manager_legacy.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
-ML_file "Tools/Sledgehammer/sledgehammer.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
+ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
end
--- a/src/HOL/Statespace/DistinctTreeProver.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Sun Jan 06 15:11:13 2019 +0100
@@ -630,6 +630,6 @@
text \<open>Now we have all the theorems in place that are needed for the
certificate generating ML functions.\<close>
-ML_file "distinct_tree_prover.ML"
+ML_file \<open>distinct_tree_prover.ML\<close>
end
--- a/src/HOL/Statespace/StateSpaceLocale.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,8 +8,8 @@
keywords "statespace" :: thy_decl
begin
-ML_file "state_space.ML"
-ML_file "state_fun.ML"
+ML_file \<open>state_space.ML\<close>
+ML_file \<open>state_fun.ML\<close>
text \<open>For every type that is to be stored in a state space, an
instance of this locale is imported in order convert the abstract and
--- a/src/HOL/String.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/String.thy Sun Jan 06 15:11:13 2019 +0100
@@ -200,7 +200,7 @@
syntax
"_String" :: "str_position \<Rightarrow> string" ("_")
-ML_file "Tools/string_syntax.ML"
+ML_file \<open>Tools/string_syntax.ML\<close>
instantiation char :: enum
begin
@@ -458,7 +458,7 @@
"_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _")
"_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _")
-ML_file "Tools/literal.ML"
+ML_file \<open>Tools/literal.ML\<close>
subsubsection \<open>Operations\<close>
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
begin
-ML_file "sledgehammer_tactics.ML"
+ML_file \<open>sledgehammer_tactics.ML\<close>
ML \<open>Proofterm.proofs := 0\<close>
@@ -18,7 +18,7 @@
declare [[unify_search_bound = 60]]
declare [[unify_trace_bound = 60]]
-ML_file "atp_problem_import.ML"
+ML_file \<open>atp_problem_import.ML\<close>
(*
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Complex_Main
begin
-ML_file "atp_theory_export.ML"
+ML_file \<open>atp_theory_export.ML\<close>
ML \<open>
open ATP_Problem
--- a/src/HOL/TPTP/MaSh_Eval.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports MaSh_Export_Base
begin
-ML_file "mash_eval.ML"
+ML_file \<open>mash_eval.ML\<close>
sledgehammer_params
[provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
--- a/src/HOL/TPTP/MaSh_Export_Base.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
imports Main
begin
-ML_file "mash_export.ML"
+ML_file \<open>mash_export.ML\<close>
sledgehammer_params
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
--- a/src/HOL/TPTP/TPTP_Interpret.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret.thy Sun Jan 06 15:11:13 2019 +0100
@@ -12,6 +12,6 @@
typedecl ind
-ML_file "TPTP_Parser/tptp_interpret.ML"
+ML_file \<open>TPTP_Parser/tptp_interpret.ML\<close>
end
--- a/src/HOL/TPTP/TPTP_Parser.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/TPTP_Parser.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,13 +8,13 @@
imports Pure
begin
-ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
+ML_file \<open>TPTP_Parser/ml_yacc_lib.ML\<close> (*generated from ML-Yacc's lib*)
-ML_file "TPTP_Parser/tptp_syntax.ML"
-ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
-ML_file "TPTP_Parser/tptp_parser.ML"
-ML_file "TPTP_Parser/tptp_problem_name.ML"
-ML_file "TPTP_Parser/tptp_proof.ML"
+ML_file \<open>TPTP_Parser/tptp_syntax.ML\<close>
+ML_file \<open>TPTP_Parser/tptp_lexyacc.ML\<close> (*generated from tptp.lex and tptp.yacc*)
+ML_file \<open>TPTP_Parser/tptp_parser.ML\<close>
+ML_file \<open>TPTP_Parser/tptp_problem_name.ML\<close>
+ML_file \<open>TPTP_Parser/tptp_proof.ML\<close>
text \<open>The TPTP parser was generated using ML-Yacc, and needs the
ML-Yacc library to operate. This library is included with the parser,
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Jan 06 15:11:13 2019 +0100
@@ -75,9 +75,9 @@
tptp_informative_failure = true
]]
-ML_file "TPTP_Parser/tptp_reconstruct_library.ML"
+ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close>
ML "open TPTP_Reconstruct_Library"
-ML_file "TPTP_Parser/tptp_reconstruct.ML"
+ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close>
(*FIXME fudge*)
declare [[
--- a/src/HOL/Transfer.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Transfer.thy Sun Jan 06 15:11:13 2019 +0100
@@ -230,7 +230,7 @@
-ML_file "Tools/Transfer/transfer.ML"
+ML_file \<open>Tools/Transfer/transfer.ML\<close>
declare refl [transfer_rule]
hide_const (open) Rel
@@ -362,8 +362,8 @@
"(if \<not> P then t else e) = (if P then e else t)"
by auto
-ML_file "Tools/Transfer/transfer_bnf.ML"
-ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
+ML_file \<open>Tools/Transfer/transfer_bnf.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_transfer.ML\<close>
declare pred_fun_def [simp]
declare rel_fun_eq [relator_eq]
--- a/src/HOL/Transitive_Closure.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Transitive_Closure.thy Sun Jan 06 15:11:13 2019 +0100
@@ -12,7 +12,7 @@
and "^=" = "\<^sup>=" "\<^sup>=\<^sup>="
begin
-ML_file "~~/src/Provers/trancl.ML"
+ML_file \<open>~~/src/Provers/trancl.ML\<close>
text \<open>
\<open>rtrancl\<close> is reflexive/transitive closure,
--- a/src/HOL/Typedef.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Typedef.thy Sun Jan 06 15:11:13 2019 +0100
@@ -108,6 +108,6 @@
end
-ML_file "Tools/typedef.ML"
+ML_file \<open>Tools/typedef.ML\<close>
end
--- a/src/HOL/Types_To_Sets/Types_To_Sets.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy Sun Jan 06 15:11:13 2019 +0100
@@ -16,13 +16,13 @@
subsection \<open>Rules\<close>
text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
-ML_file "local_typedef.ML"
+ML_file \<open>local_typedef.ML\<close>
text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
-ML_file "unoverloading.ML"
+ML_file \<open>unoverloading.ML\<close>
text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
-ML_file "internalize_sort.ML"
+ML_file \<open>internalize_sort.ML\<close>
text\<open>The following file provides some automation to unoverload and internalize the parameters o
the sort constraints of a type variable.\<close>
--- a/src/HOL/UNITY/UNITY_Main.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
imports Detects PPROD Follows ProgressSets
begin
-ML_file "UNITY_tactics.ML"
+ML_file \<open>UNITY_tactics.ML\<close>
method_setup safety = \<open>
Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close>
--- a/src/HOL/Word/Word.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Word/Word.thy Sun Jan 06 15:11:13 2019 +0100
@@ -4502,8 +4502,8 @@
declare bin_to_bl_def [simp]
-ML_file "Tools/word_lib.ML"
-ML_file "Tools/smt_word.ML"
+ML_file \<open>Tools/word_lib.ML\<close>
+ML_file \<open>Tools/smt_word.ML\<close>
hide_const (open) Word
--- a/src/HOL/ex/Cartouche_Examples.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Sun Jan 06 15:11:13 2019 +0100
@@ -123,11 +123,11 @@
text \<open>
\<^ML>\<open>
(
- @{term \<open>""\<close>};
- @{term \<open>"abc"\<close>};
- @{term \<open>"abc" @ "xyz"\<close>};
- @{term \<open>"\<newline>"\<close>};
- @{term \<open>"\001\010\100"\<close>}
+ \<^term>\<open>""\<close>;
+ \<^term>\<open>"abc"\<close>;
+ \<^term>\<open>"abc" @ "xyz"\<close>;
+ \<^term>\<open>"\<newline>"\<close>;
+ \<^term>\<open>"\001\010\100"\<close>
)
\<close>
\<close>
@@ -146,11 +146,11 @@
\<open>
\<^ML>\<open>
(
- @{term \<open>""\<close>};
- @{term \<open>"abc"\<close>};
- @{term \<open>"abc" @ "xyz"\<close>};
- @{term \<open>"\<newline>"\<close>};
- @{term \<open>"\001\010\100"\<close>}
+ \<^term>\<open>""\<close>;
+ \<^term>\<open>"abc"\<close>;
+ \<^term>\<open>"abc" @ "xyz"\<close>;
+ \<^term>\<open>"\<newline>"\<close>;
+ \<^term>\<open>"\001\010\100"\<close>
)
\<close>
\<close>
--- a/src/Pure/Isar/token.scala Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Pure/Isar/token.scala Sun Jan 06 15:11:13 2019 +0100
@@ -156,6 +156,15 @@
val newline: Token = explode(Keyword.Keywords.empty, "\n").head
+ /* embedded */
+
+ def read_embedded(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
+ explode(keywords, inp) match {
+ case List(tok) if tok.is_embedded => Some(tok)
+ case _ => None
+ }
+
+
/* names */
def read_name(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
--- a/src/Pure/Tools/update.scala Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Pure/Tools/update.scala Sun Jan 06 15:11:13 2019 +0100
@@ -31,10 +31,18 @@
session_dirs = dirs ::: select_dirs,
include_sessions = deps.sessions_structure.imports_topological_order)
+ val path_cartouches = dump_options.bool("update_path_cartouches")
+
def update_xml(xml: XML.Body): XML.Body =
xml flatMap {
case XML.Wrapped_Elem(markup, body1, body2) =>
if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
+ case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body)
+ if path_cartouches =>
+ Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
+ case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
+ case None => update_xml(body)
+ }
case XML.Elem(_, body) => update_xml(body)
case t => List(t)
}
@@ -48,7 +56,7 @@
for ((node_name, node) <- snapshot.nodes) {
val xml =
snapshot.state.markup_to_XML(snapshot.version, node_name,
- Text.Range.full, Markup.Elements(Markup.UPDATE))
+ Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
val source1 = Symbol.encode(XML.content(update_xml(xml)))
if (source1 != Symbol.encode(node.source)) {
--- a/src/Sequents/LK.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Sequents/LK.thy Sun Jan 06 15:11:13 2019 +0100
@@ -200,7 +200,7 @@
lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x"
by (fast add!: subst)
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
setup \<open>map_theory_simpset (put_simpset LK_ss)\<close>
setup \<open>Simplifier.method_setup []\<close>
--- a/src/Sequents/Modal0.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Sequents/Modal0.thy Sun Jan 06 15:11:13 2019 +0100
@@ -7,7 +7,7 @@
imports LK0
begin
-ML_file "modal.ML"
+ML_file \<open>modal.ML\<close>
consts
box :: "o\<Rightarrow>o" ("[]_" [50] 50)
--- a/src/Sequents/Sequents.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Sequents/Sequents.thy Sun Jan 06 15:11:13 2019 +0100
@@ -144,6 +144,6 @@
subsection \<open>Proof tools\<close>
-ML_file "prover.ML"
+ML_file \<open>prover.ML\<close>
end
--- a/src/Tools/Code_Generator.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Tools/Code_Generator.thy Sun Jan 06 15:11:13 2019 +0100
@@ -16,17 +16,17 @@
:: quasi_command
begin
-ML_file "~~/src/Tools/cache_io.ML"
-ML_file "~~/src/Tools/Code/code_preproc.ML"
-ML_file "~~/src/Tools/Code/code_symbol.ML"
-ML_file "~~/src/Tools/Code/code_thingol.ML"
-ML_file "~~/src/Tools/Code/code_simp.ML"
-ML_file "~~/src/Tools/Code/code_printer.ML"
-ML_file "~~/src/Tools/Code/code_target.ML"
-ML_file "~~/src/Tools/Code/code_namespace.ML"
-ML_file "~~/src/Tools/Code/code_ml.ML"
-ML_file "~~/src/Tools/Code/code_haskell.ML"
-ML_file "~~/src/Tools/Code/code_scala.ML"
+ML_file \<open>~~/src/Tools/cache_io.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_preproc.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_symbol.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_thingol.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_simp.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_printer.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_target.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_namespace.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_ml.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_haskell.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_scala.ML\<close>
code_datatype "TYPE('a::{})"
@@ -55,8 +55,8 @@
by rule (rule holds)+
qed
-ML_file "~~/src/Tools/Code/code_runtime.ML"
-ML_file "~~/src/Tools/nbe.ML"
+ML_file \<open>~~/src/Tools/Code/code_runtime.ML\<close>
+ML_file \<open>~~/src/Tools/nbe.ML\<close>
hide_const (open) holds
--- a/src/Tools/SML/Examples.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Tools/SML/Examples.thy Sun Jan 06 15:11:13 2019 +0100
@@ -21,7 +21,7 @@
evaluates it for some arguments.
\<close>
-SML_file "factorial.sml"
+SML_file \<open>factorial.sml\<close>
text \<open>
The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands
@@ -30,8 +30,8 @@
independently of the Isabelle/ML environment.
\<close>
-SML_file "Example.sig"
-SML_file "Example.sml"
+SML_file \<open>Example.sig\<close>
+SML_file \<open>Example.sml\<close>
text \<open>
--- a/src/Tools/Spec_Check/Spec_Check.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Tools/Spec_Check/Spec_Check.thy Sun Jan 06 15:11:13 2019 +0100
@@ -2,12 +2,12 @@
imports Pure
begin
-ML_file "random.ML"
-ML_file "property.ML"
-ML_file "base_generator.ML"
-ML_file "generator.ML"
-ML_file "gen_construction.ML"
-ML_file "spec_check.ML"
-ML_file "output_style.ML"
+ML_file \<open>random.ML\<close>
+ML_file \<open>property.ML\<close>
+ML_file \<open>base_generator.ML\<close>
+ML_file \<open>generator.ML\<close>
+ML_file \<open>gen_construction.ML\<close>
+ML_file \<open>spec_check.ML\<close>
+ML_file \<open>output_style.ML\<close>
end
\ No newline at end of file
--- a/src/ZF/ArithSimp.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/ArithSimp.thy Sun Jan 06 15:11:13 2019 +0100
@@ -9,9 +9,9 @@
imports Arith
begin
-ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
-ML_file "~~/src/Provers/Arith/combine_numerals.ML"
-ML_file "arith_data.ML"
+ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
+ML_file \<open>arith_data.ML\<close>
subsection\<open>Difference\<close>
--- a/src/ZF/Bin.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/Bin.thy Sun Jan 06 15:11:13 2019 +0100
@@ -117,7 +117,7 @@
"_Int" :: "num_token => i" (\<open>#_\<close> 1000)
"_Neg_Int" :: "num_token => i" (\<open>#-_\<close> 1000)
-ML_file "Tools/numeral_syntax.ML"
+ML_file \<open>Tools/numeral_syntax.ML\<close>
declare bin.intros [simp,TC]
@@ -698,7 +698,7 @@
apply (simp add: zadd_ac)
done
-ML_file "int_arith.ML"
+ML_file \<open>int_arith.ML\<close>
subsection \<open>examples:\<close>
--- a/src/ZF/Datatype.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/Datatype.thy Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
keywords "datatype" "codatatype" :: thy_decl
begin
-ML_file "Tools/datatype_package.ML"
+ML_file \<open>Tools/datatype_package.ML\<close>
ML \<open>
(*Typechecking rules for most datatypes involving univ*)
--- a/src/ZF/Inductive.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/Inductive.thy Sun Jan 06 15:11:13 2019 +0100
@@ -27,12 +27,12 @@
lemma refl_thin: "!!P. a = a ==> P ==> P" .
-ML_file "ind_syntax.ML"
-ML_file "Tools/ind_cases.ML"
-ML_file "Tools/cartprod.ML"
-ML_file "Tools/inductive_package.ML"
-ML_file "Tools/induct_tacs.ML"
-ML_file "Tools/primrec_package.ML"
+ML_file \<open>ind_syntax.ML\<close>
+ML_file \<open>Tools/ind_cases.ML\<close>
+ML_file \<open>Tools/cartprod.ML\<close>
+ML_file \<open>Tools/inductive_package.ML\<close>
+ML_file \<open>Tools/induct_tacs.ML\<close>
+ML_file \<open>Tools/primrec_package.ML\<close>
ML \<open>
structure Lfp =
--- a/src/ZF/pair.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/pair.thy Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
theory pair imports upair
begin
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
setup \<open>
map_theory_simpset
--- a/src/ZF/upair.thy Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/upair.thy Sun Jan 06 15:11:13 2019 +0100
@@ -16,7 +16,7 @@
keywords "print_tcset" :: diag
begin
-ML_file "Tools/typechk.ML"
+ML_file \<open>Tools/typechk.ML\<close>
lemma atomize_ball [symmetric, rulify]:
"(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"