# HG changeset patch # User wenzelm # Date 1248461756 -7200 # Node ID 34f7b0fbe047f516b5dd6de8738ae2c9831be14e # Parent c4e55f30d527150cefd6b9b45db8e2f3a7f7a60c structure OldGoals: no pervasive names; diff -r c4e55f30d527 -r 34f7b0fbe047 src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Fri Jul 24 18:58:58 2009 +0200 +++ b/src/Pure/old_goals.ML Fri Jul 24 20:55:56 2009 +0200 @@ -8,28 +8,48 @@ may be a stack of pending proofs. *) -signature GOALS = +signature OLD_GOALS = sig val the_context: unit -> theory + val simple_read_term: theory -> typ -> string -> term + val read_term: theory -> string -> term + val read_prop: theory -> string -> term + type proof val premises: unit -> thm list + val reset_goals: unit -> unit + val result_error_fn: (thm -> string -> thm) ref + val print_sign_exn: theory -> exn -> 'a + val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm + val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm + val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm val prove_goal: theory -> string -> (thm list -> tactic list) -> thm - val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm val topthm: unit -> thm val result: unit -> thm val uresult: unit -> thm val getgoal: int -> term val gethyps: int -> thm list + val print_exn: exn -> 'a + val filter_goal: (term*term->bool) -> thm list -> int -> thm list val prlev: int -> unit val pr: unit -> unit val prlim: int -> unit + val goalw_cterm: thm list -> cterm -> thm list + val goalw: theory -> thm list -> string -> thm list val goal: theory -> string -> thm list - val goalw: theory -> thm list -> string -> thm list + val Goalw: thm list -> string -> thm list val Goal: string -> thm list - val Goalw: thm list -> string -> thm list + val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm val by: tactic -> unit + val byev: tactic list -> unit val back: unit -> unit val choplev: int -> unit + val chop: unit -> unit val undo: unit -> unit + val save_proof: unit -> proof + val restore_proof: proof -> thm list + val push_proof: unit -> unit + val pop_proof: unit -> thm list + val rotate_proof: unit -> thm list val qed: string -> unit val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit val qed_goalw: string -> theory -> thm list -> string @@ -40,31 +60,6 @@ -> (thm list -> tactic list) -> unit end; -signature OLD_GOALS = -sig - include GOALS - val simple_read_term: theory -> typ -> string -> term - val read_term: theory -> string -> term - val read_prop: theory -> string -> term - type proof - val chop: unit -> unit - val reset_goals: unit -> unit - val result_error_fn: (thm -> string -> thm) ref - val print_sign_exn: theory -> exn -> 'a - val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm - val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm - val print_exn: exn -> 'a - val filter_goal: (term*term->bool) -> thm list -> int -> thm list - val goalw_cterm: thm list -> cterm -> thm list - val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm - val byev: tactic list -> unit - val save_proof: unit -> proof - val restore_proof: proof -> thm list - val push_proof: unit -> unit - val pop_proof: unit -> thm list - val rotate_proof: unit -> thm list -end; - structure OldGoals: OLD_GOALS = struct @@ -457,12 +452,13 @@ in proofstack := ps; pr(); prems end; (* rotate the stack so that the top element goes to the bottom *) -fun rotate_proof() = let val (p,ps) = top_proof() - in proofstack := ps@[save_proof()]; - restore_proof p; - pr(); - !curr_prems - end; +fun rotate_proof() = + let val (p,ps) = top_proof() + in proofstack := ps@[save_proof()]; + restore_proof p; + pr(); + !curr_prems + end; (** theorem bindings **) @@ -480,5 +476,3 @@ end; -structure Goals: GOALS = OldGoals; -open Goals;