# HG changeset patch # User wenzelm # Date 1395157491 -3600 # Node ID 7adec2a527f5315f1dad239bdb83dcc06ae1b9f6 # Parent ceb8a93460b7abc03a05c3fd48d324b15dd82c38 clarified module arrangement; more antiquotations; diff -r ceb8a93460b7 -r 7adec2a527f5 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Mar 18 16:16:28 2014 +0100 +++ b/src/Pure/Proof/extraction.ML Tue Mar 18 16:44:51 2014 +0100 @@ -466,9 +466,9 @@ "(realizes (r) (!!x. PROP P (x))) == \ \ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #> - Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false)) + Attrib.setup @{binding extraction_expand} (Scan.succeed (extraction_expand false)) "specify theorems to be expanded during extraction" #> - Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true)) + Attrib.setup @{binding extraction_expand_def} (Scan.succeed (extraction_expand true)) "specify definitions to be expanded during extraction"); diff -r ceb8a93460b7 -r 7adec2a527f5 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Mar 18 16:16:28 2014 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Tue Mar 18 16:44:51 2014 +0100 @@ -63,9 +63,9 @@ ("", idtT --> paramsT, Delimfix "_"), ("", paramT --> paramsT, Delimfix "_")] |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) - [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3)), - (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), - (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] + [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), + (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), + (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4))] |> Sign.add_trrules (map Syntax.Parse_Print_Rule [(Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam0") diff -r ceb8a93460b7 -r 7adec2a527f5 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Mar 18 16:16:28 2014 +0100 +++ b/src/Pure/ROOT.ML Tue Mar 18 16:44:51 2014 +0100 @@ -211,12 +211,6 @@ use "Syntax/syntax_phases.ML"; use "Isar/local_defs.ML"; -(*proof term operations*) -use "Proof/reconstruct.ML"; -use "Proof/proof_syntax.ML"; -use "Proof/proof_rewrite_rules.ML"; -use "Proof/proof_checker.ML"; - (*outer syntax*) use "Isar/token.ML"; use "Isar/keyword.ML"; @@ -271,6 +265,13 @@ use "Isar/proof_node.ML"; use "Isar/toplevel.ML"; +(*proof term operations*) +use "Proof/reconstruct.ML"; +use "Proof/proof_syntax.ML"; +use "Proof/proof_rewrite_rules.ML"; +use "Proof/proof_checker.ML"; +use "Proof/extraction.ML"; + (*theory documents*) use "System/isabelle_system.ML"; use "Thy/term_style.ML"; @@ -290,8 +291,6 @@ use "subgoal.ML"; -use "Proof/extraction.ML"; - (* Isabelle/Isar system *)