clarified module arrangement;
authorwenzelm
Tue Mar 18 16:44:51 2014 +0100 (2014-03-18)
changeset 562067adec2a527f5
parent 56205 ceb8a93460b7
child 56207 52d5067ca06a
clarified module arrangement;
more antiquotations;
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 18 16:16:28 2014 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 18 16:44:51 2014 +0100
     1.3 @@ -466,9 +466,9 @@
     1.4        "(realizes (r) (!!x. PROP P (x))) ==  \
     1.5      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
     1.6  
     1.7 -   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
     1.8 +   Attrib.setup @{binding extraction_expand} (Scan.succeed (extraction_expand false))
     1.9       "specify theorems to be expanded during extraction" #>
    1.10 -   Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
    1.11 +   Attrib.setup @{binding extraction_expand_def} (Scan.succeed (extraction_expand true))
    1.12       "specify definitions to be expanded during extraction");
    1.13  
    1.14  
     2.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Mar 18 16:16:28 2014 +0100
     2.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Mar 18 16:44:51 2014 +0100
     2.3 @@ -63,9 +63,9 @@
     2.4         ("", idtT --> paramsT, Delimfix "_"),
     2.5         ("", paramT --> paramsT, Delimfix "_")]
     2.6    |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
     2.7 -      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3)),
     2.8 -       (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
     2.9 -       (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
    2.10 +      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
    2.11 +       (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
    2.12 +       (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
    2.13    |> Sign.add_trrules (map Syntax.Parse_Print_Rule
    2.14        [(Ast.mk_appl (Ast.Constant "_Lam")
    2.15            [Ast.mk_appl (Ast.Constant "_Lam0")
     3.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 16:16:28 2014 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 16:44:51 2014 +0100
     3.3 @@ -211,12 +211,6 @@
     3.4  use "Syntax/syntax_phases.ML";
     3.5  use "Isar/local_defs.ML";
     3.6  
     3.7 -(*proof term operations*)
     3.8 -use "Proof/reconstruct.ML";
     3.9 -use "Proof/proof_syntax.ML";
    3.10 -use "Proof/proof_rewrite_rules.ML";
    3.11 -use "Proof/proof_checker.ML";
    3.12 -
    3.13  (*outer syntax*)
    3.14  use "Isar/token.ML";
    3.15  use "Isar/keyword.ML";
    3.16 @@ -271,6 +265,13 @@
    3.17  use "Isar/proof_node.ML";
    3.18  use "Isar/toplevel.ML";
    3.19  
    3.20 +(*proof term operations*)
    3.21 +use "Proof/reconstruct.ML";
    3.22 +use "Proof/proof_syntax.ML";
    3.23 +use "Proof/proof_rewrite_rules.ML";
    3.24 +use "Proof/proof_checker.ML";
    3.25 +use "Proof/extraction.ML";
    3.26 +
    3.27  (*theory documents*)
    3.28  use "System/isabelle_system.ML";
    3.29  use "Thy/term_style.ML";
    3.30 @@ -290,8 +291,6 @@
    3.31  
    3.32  use "subgoal.ML";
    3.33  
    3.34 -use "Proof/extraction.ML";
    3.35 -
    3.36  
    3.37  (* Isabelle/Isar system *)
    3.38