src/Pure/Isar/isar_syn.ML
changeset 21350 6e58289b6685
parent 21306 7ab6e95e6b0b
child 21403 dd58f13a8eb4
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 14 00:15:37 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 14 00:15:38 2006 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  val theoryP =
     1.6    OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
     1.7 -    (ThyHeader.args >> (Toplevel.print oo IsarThy.theory));
     1.8 +    (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory));
     1.9  
    1.10  val endP =
    1.11    OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
    1.12 @@ -174,7 +174,7 @@
    1.13  
    1.14  val axiomsP =
    1.15    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
    1.16 -    (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
    1.17 +    (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
    1.18  
    1.19  val opt_unchecked_overloaded =
    1.20    Scan.optional (P.$$$ "(" |-- P.!!!
    1.21 @@ -184,7 +184,7 @@
    1.22  val defsP =
    1.23    OuterSyntax.command "defs" "define constants" K.thy_decl
    1.24      (opt_unchecked_overloaded -- Scan.repeat1 P.spec_name
    1.25 -      >> (Toplevel.theory o IsarThy.add_defs));
    1.26 +      >> (Toplevel.theory o IsarCmd.add_defs));
    1.27  
    1.28  
    1.29  (* constant definitions and abbreviations *)
    1.30 @@ -399,22 +399,22 @@
    1.31  val haveP =
    1.32    OuterSyntax.command "have" "state local goal"
    1.33      (K.tag_proof K.prf_goal)
    1.34 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.have));
    1.35 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
    1.36  
    1.37  val henceP =
    1.38    OuterSyntax.command "hence" "abbreviates \"then have\""
    1.39      (K.tag_proof K.prf_goal)
    1.40 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.hence));
    1.41 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
    1.42  
    1.43  val showP =
    1.44    OuterSyntax.command "show" "state local goal, solving current obligation"
    1.45      (K.tag_proof K.prf_goal)
    1.46 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show));
    1.47 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
    1.48  
    1.49  val thusP =
    1.50    OuterSyntax.command "thus" "abbreviates \"then show\""
    1.51      (K.tag_proof K.prf_goal)
    1.52 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus));
    1.53 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
    1.54  
    1.55  
    1.56  (* facts *)
    1.57 @@ -527,32 +527,32 @@
    1.58  val qedP =
    1.59    OuterSyntax.command "qed" "conclude (sub-)proof"
    1.60      (K.tag_proof K.qed_block)
    1.61 -    (Scan.option P.method >> (Toplevel.print3 oo IsarThy.qed));
    1.62 +    (Scan.option P.method >> (Toplevel.print3 oo IsarCmd.qed));
    1.63  
    1.64  val terminal_proofP =
    1.65    OuterSyntax.command "by" "terminal backward proof"
    1.66      (K.tag_proof K.qed)
    1.67 -    (P.method -- Scan.option P.method >> (Toplevel.print3 oo IsarThy.terminal_proof));
    1.68 +    (P.method -- Scan.option P.method >> (Toplevel.print3 oo IsarCmd.terminal_proof));
    1.69  
    1.70  val default_proofP =
    1.71    OuterSyntax.command ".." "default proof"
    1.72      (K.tag_proof K.qed)
    1.73 -    (Scan.succeed (Toplevel.print3 o IsarThy.default_proof));
    1.74 +    (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof));
    1.75  
    1.76  val immediate_proofP =
    1.77    OuterSyntax.command "." "immediate proof"
    1.78      (K.tag_proof K.qed)
    1.79 -    (Scan.succeed (Toplevel.print3 o IsarThy.immediate_proof));
    1.80 +    (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof));
    1.81  
    1.82  val done_proofP =
    1.83    OuterSyntax.command "done" "done proof"
    1.84      (K.tag_proof K.qed)
    1.85 -    (Scan.succeed (Toplevel.print3 o IsarThy.done_proof));
    1.86 +    (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
    1.87  
    1.88  val skip_proofP =
    1.89    OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
    1.90      (K.tag_proof K.qed)
    1.91 -    (Scan.succeed (Toplevel.print3 o IsarThy.skip_proof));
    1.92 +    (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
    1.93  
    1.94  val forget_proofP =
    1.95    OuterSyntax.command "oops" "forget proof"