src/Pure/old_goals.ML
changeset 27242 9a1b82f7b6a8
parent 27233 224c830e7abe
child 27256 bcb071683184
     1.1 --- a/src/Pure/old_goals.ML	Mon Jun 16 22:13:47 2008 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Mon Jun 16 22:13:49 2008 +0200
     1.3 @@ -39,7 +39,6 @@
     1.4    val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit
     1.5    val qed_goalw_spec_mp: string -> theory -> thm list -> string
     1.6      -> (thm list -> tactic list) -> unit
     1.7 -  val no_qed: unit -> unit
     1.8  end;
     1.9  
    1.10  signature OLD_GOALS =
    1.11 @@ -52,8 +51,6 @@
    1.12    val print_sign_exn: theory -> exn -> 'a
    1.13    val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
    1.14    val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
    1.15 -  val quick_and_dirty_prove_goalw_cterm: theory -> thm list -> cterm
    1.16 -    -> (thm list -> tactic list) -> thm
    1.17    val print_exn: exn -> 'a
    1.18    val filter_goal: (term*term->bool) -> thm list -> int -> thm list
    1.19    val goalw_cterm: thm list -> cterm -> thm list
    1.20 @@ -64,23 +61,6 @@
    1.21    val push_proof: unit -> unit
    1.22    val pop_proof: unit -> thm list
    1.23    val rotate_proof: unit -> thm list
    1.24 -  val bws: thm list -> unit
    1.25 -  val bw: thm -> unit
    1.26 -  val brs: thm list -> int -> unit
    1.27 -  val br: thm -> int -> unit
    1.28 -  val bes: thm list -> int -> unit
    1.29 -  val be: thm -> int -> unit
    1.30 -  val bds: thm list -> int -> unit
    1.31 -  val bd: thm -> int -> unit
    1.32 -  val ba: int -> unit
    1.33 -  val ren: string -> int -> unit
    1.34 -  val frs: thm list -> unit
    1.35 -  val fr: thm -> unit
    1.36 -  val fes: thm list -> unit
    1.37 -  val fe: thm -> unit
    1.38 -  val fds: thm list -> unit
    1.39 -  val fd: thm -> unit
    1.40 -  val fa: unit -> unit
    1.41  end;
    1.42  
    1.43  structure OldGoals: OLD_GOALS =
    1.44 @@ -252,10 +232,6 @@
    1.45  (*String version with no meta-rewrite-rules*)
    1.46  fun prove_goal thy = prove_goalw thy [];
    1.47  
    1.48 -(*quick and dirty version (conditional)*)
    1.49 -fun quick_and_dirty_prove_goalw_cterm thy rews ct tacs =
    1.50 -  prove_goalw_cterm rews ct
    1.51 -    (if ! quick_and_dirty then (K [SkipProof.cheat_tac thy]) else tacs);
    1.52  
    1.53  
    1.54  (*** Commands etc ***)
    1.55 @@ -469,38 +445,6 @@
    1.56                      end;
    1.57  
    1.58  
    1.59 -(** Shortcuts for commonly-used tactics **)
    1.60 -
    1.61 -fun bws rls = by (rewrite_goals_tac rls);
    1.62 -fun bw rl = bws [rl];
    1.63 -
    1.64 -fun brs rls i = by (resolve_tac rls i);
    1.65 -fun br rl = brs [rl];
    1.66 -
    1.67 -fun bes rls i = by (eresolve_tac rls i);
    1.68 -fun be rl = bes [rl];
    1.69 -
    1.70 -fun bds rls i = by (dresolve_tac rls i);
    1.71 -fun bd rl = bds [rl];
    1.72 -
    1.73 -fun ba i = by (assume_tac i);
    1.74 -
    1.75 -fun ren str i = by (rename_tac str i);
    1.76 -
    1.77 -(** Shortcuts to work on the first applicable subgoal **)
    1.78 -
    1.79 -fun frs rls = by (FIRSTGOAL (trace_goalno_tac (resolve_tac rls)));
    1.80 -fun fr rl = frs [rl];
    1.81 -
    1.82 -fun fes rls = by (FIRSTGOAL (trace_goalno_tac (eresolve_tac rls)));
    1.83 -fun fe rl = fes [rl];
    1.84 -
    1.85 -fun fds rls = by (FIRSTGOAL (trace_goalno_tac (dresolve_tac rls)));
    1.86 -fun fd rl = fds [rl];
    1.87 -
    1.88 -fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac));
    1.89 -
    1.90 -
    1.91  (** theorem bindings **)
    1.92  
    1.93  fun qed name = ML_Context.ml_store_thm (name, result ());
    1.94 @@ -514,8 +458,6 @@
    1.95  fun qed_goalw_spec_mp name thy defs s p =
    1.96    bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
    1.97  
    1.98 -fun no_qed () = ();
    1.99 -
   1.100  end;
   1.101  
   1.102  structure Goals: GOALS = OldGoals;