src/Pure/old_goals.ML
changeset 32173 34f7b0fbe047
parent 32145 220c9e439d39
child 32179 1c9c991e41c0
     1.1 --- a/src/Pure/old_goals.ML	Fri Jul 24 18:58:58 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Fri Jul 24 20:55:56 2009 +0200
     1.3 @@ -8,28 +8,48 @@
     1.4  may be a stack of pending proofs.
     1.5  *)
     1.6  
     1.7 -signature GOALS =
     1.8 +signature OLD_GOALS =
     1.9  sig
    1.10    val the_context: unit -> theory
    1.11 +  val simple_read_term: theory -> typ -> string -> term
    1.12 +  val read_term: theory -> string -> term
    1.13 +  val read_prop: theory -> string -> term
    1.14 +  type proof
    1.15    val premises: unit -> thm list
    1.16 +  val reset_goals: unit -> unit
    1.17 +  val result_error_fn: (thm -> string -> thm) ref
    1.18 +  val print_sign_exn: theory -> exn -> 'a
    1.19 +  val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
    1.20 +  val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
    1.21 +  val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm
    1.22    val prove_goal: theory -> string -> (thm list -> tactic list) -> thm
    1.23 -  val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm
    1.24    val topthm: unit -> thm
    1.25    val result: unit -> thm
    1.26    val uresult: unit -> thm
    1.27    val getgoal: int -> term
    1.28    val gethyps: int -> thm list
    1.29 +  val print_exn: exn -> 'a
    1.30 +  val filter_goal: (term*term->bool) -> thm list -> int -> thm list
    1.31    val prlev: int -> unit
    1.32    val pr: unit -> unit
    1.33    val prlim: int -> unit
    1.34 +  val goalw_cterm: thm list -> cterm -> thm list
    1.35 +  val goalw: theory -> thm list -> string -> thm list
    1.36    val goal: theory -> string -> thm list
    1.37 -  val goalw: theory -> thm list -> string -> thm list
    1.38 +  val Goalw: thm list -> string -> thm list
    1.39    val Goal: string -> thm list
    1.40 -  val Goalw: thm list -> string -> thm list
    1.41 +  val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm
    1.42    val by: tactic -> unit
    1.43 +  val byev: tactic list -> unit
    1.44    val back: unit -> unit
    1.45    val choplev: int -> unit
    1.46 +  val chop: unit -> unit
    1.47    val undo: unit -> unit
    1.48 +  val save_proof: unit -> proof
    1.49 +  val restore_proof: proof -> thm list
    1.50 +  val push_proof: unit -> unit
    1.51 +  val pop_proof: unit -> thm list
    1.52 +  val rotate_proof: unit -> thm list
    1.53    val qed: string -> unit
    1.54    val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
    1.55    val qed_goalw: string -> theory -> thm list -> string
    1.56 @@ -40,31 +60,6 @@
    1.57      -> (thm list -> tactic list) -> unit
    1.58  end;
    1.59  
    1.60 -signature OLD_GOALS =
    1.61 -sig
    1.62 -  include GOALS
    1.63 -  val simple_read_term: theory -> typ -> string -> term
    1.64 -  val read_term: theory -> string -> term
    1.65 -  val read_prop: theory -> string -> term
    1.66 -  type proof
    1.67 -  val chop: unit -> unit
    1.68 -  val reset_goals: unit -> unit
    1.69 -  val result_error_fn: (thm -> string -> thm) ref
    1.70 -  val print_sign_exn: theory -> exn -> 'a
    1.71 -  val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
    1.72 -  val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
    1.73 -  val print_exn: exn -> 'a
    1.74 -  val filter_goal: (term*term->bool) -> thm list -> int -> thm list
    1.75 -  val goalw_cterm: thm list -> cterm -> thm list
    1.76 -  val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm
    1.77 -  val byev: tactic list -> unit
    1.78 -  val save_proof: unit -> proof
    1.79 -  val restore_proof: proof -> thm list
    1.80 -  val push_proof: unit -> unit
    1.81 -  val pop_proof: unit -> thm list
    1.82 -  val rotate_proof: unit -> thm list
    1.83 -end;
    1.84 -
    1.85  structure OldGoals: OLD_GOALS =
    1.86  struct
    1.87  
    1.88 @@ -457,12 +452,13 @@
    1.89    in proofstack := ps;  pr();  prems end;
    1.90  
    1.91  (* rotate the stack so that the top element goes to the bottom *)
    1.92 -fun rotate_proof() = let val (p,ps) = top_proof()
    1.93 -                    in proofstack := ps@[save_proof()];
    1.94 -                       restore_proof p;
    1.95 -                       pr();
    1.96 -                       !curr_prems
    1.97 -                    end;
    1.98 +fun rotate_proof() =
    1.99 +  let val (p,ps) = top_proof()
   1.100 +  in proofstack := ps@[save_proof()];
   1.101 +     restore_proof p;
   1.102 +     pr();
   1.103 +     !curr_prems
   1.104 +  end;
   1.105  
   1.106  
   1.107  (** theorem bindings **)
   1.108 @@ -480,5 +476,3 @@
   1.109  
   1.110  end;
   1.111  
   1.112 -structure Goals: GOALS = OldGoals;
   1.113 -open Goals;