eliminated dead code;
authorwenzelm
Tue Jun 09 15:28:06 2015 +0200 (2015-06-09 ago)
changeset 60405990c9fea6773
parent 60404 422b63ef0147
child 60406 12cc54fac9b0
eliminated dead code;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 13:42:58 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 15:28:06 2015 +0200
     1.3 @@ -173,17 +173,6 @@
     1.4    |> Context.proof_map;
     1.5  
     1.6  
     1.7 -(* goals *)
     1.8 -
     1.9 -fun goal opt_chain goal stmt int =
    1.10 -  opt_chain #> goal NONE (K I) stmt int;
    1.11 -
    1.12 -val have = goal I Proof.have_cmd;
    1.13 -val hence = goal Proof.chain Proof.have_cmd;
    1.14 -val show = goal I Proof.show_cmd;
    1.15 -val thus = goal Proof.chain Proof.show_cmd;
    1.16 -
    1.17 -
    1.18  (* local endings *)
    1.19  
    1.20  fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));