src/Pure/Isar/method.ML
changeset 20289 ba7a7c56bed5
parent 20224 9c40a144ee0e
child 20335 b5eca86ef9cc
     1.1 --- a/src/Pure/Isar/method.ML	Wed Aug 02 22:26:40 2006 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Aug 02 22:26:41 2006 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    type method
     1.5    val trace_rules: bool ref
     1.6    val print_methods: theory -> unit
     1.7 -  val Method: bstring -> (Args.src -> ProofContext.context -> method) -> string -> unit
     1.8 +  val Method: bstring -> (Args.src -> Proof.context -> method) -> string -> unit
     1.9  end;
    1.10  
    1.11  signature METHOD =
    1.12 @@ -32,31 +32,31 @@
    1.13    val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
    1.14    val defer: int option -> method
    1.15    val prefer: int -> method
    1.16 -  val cheating: bool -> ProofContext.context -> method
    1.17 +  val cheating: bool -> Proof.context -> method
    1.18    val intro: thm list -> method
    1.19    val elim: thm list -> method
    1.20 -  val unfold: thm list -> ProofContext.context -> method
    1.21 -  val fold: thm list -> ProofContext.context -> method
    1.22 +  val unfold: thm list -> Proof.context -> method
    1.23 +  val fold: thm list -> Proof.context -> method
    1.24    val atomize: bool -> method
    1.25    val this: method
    1.26 -  val fact: thm list -> ProofContext.context -> method
    1.27 -  val assumption: ProofContext.context -> method
    1.28 -  val close: bool -> ProofContext.context -> method
    1.29 -  val trace: ProofContext.context -> thm list -> unit
    1.30 +  val fact: thm list -> Proof.context -> method
    1.31 +  val assumption: Proof.context -> method
    1.32 +  val close: bool -> Proof.context -> method
    1.33 +  val trace: Proof.context -> thm list -> unit
    1.34    val rule_tac: thm list -> thm list -> int -> tactic
    1.35 -  val some_rule_tac: thm list -> ProofContext.context -> thm list -> int -> tactic
    1.36 +  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
    1.37    val rule: thm list -> method
    1.38    val erule: int -> thm list -> method
    1.39    val drule: int -> thm list -> method
    1.40    val frule: int -> thm list -> method
    1.41 -  val iprover_tac: ProofContext.context -> int option -> int -> tactic
    1.42 -  val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list ->
    1.43 +  val iprover_tac: Proof.context -> int option -> int -> tactic
    1.44 +  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
    1.45      thm -> int -> tactic
    1.46 -  val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit
    1.47 -  val tactic: string -> ProofContext.context -> method
    1.48 +  val set_tactic: (Proof.context -> thm list -> tactic) -> unit
    1.49 +  val tactic: string -> Proof.context -> method
    1.50    type src
    1.51    datatype text =
    1.52 -    Basic of (ProofContext.context -> method) |
    1.53 +    Basic of (Proof.context -> method) |
    1.54      Source of src |
    1.55      Source_i of src |
    1.56      Then of text list |
    1.57 @@ -72,45 +72,45 @@
    1.58    val sorry_text: bool -> text
    1.59    val finish_text: text option * bool -> text
    1.60    exception METHOD_FAIL of (string * Position.T) * exn
    1.61 -  val method: theory -> src -> ProofContext.context -> method
    1.62 -  val method_i: theory -> src -> ProofContext.context -> method
    1.63 -  val add_methods: (bstring * (src -> ProofContext.context -> method) * string) list
    1.64 +  val method: theory -> src -> Proof.context -> method
    1.65 +  val method_i: theory -> src -> Proof.context -> method
    1.66 +  val add_methods: (bstring * (src -> Proof.context -> method) * string) list
    1.67      -> theory -> theory
    1.68 -  val add_method: bstring * (src -> ProofContext.context -> method) * string
    1.69 +  val add_method: bstring * (src -> Proof.context -> method) * string
    1.70      -> theory -> theory
    1.71    val method_setup: bstring * string * string -> theory -> theory
    1.72    val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
    1.73 -    -> src -> ProofContext.context -> ProofContext.context * 'a
    1.74 +    -> src -> Proof.context -> Proof.context * 'a
    1.75    val simple_args: (Args.T list -> 'a * Args.T list)
    1.76 -    -> ('a -> ProofContext.context -> method) -> src -> ProofContext.context -> method
    1.77 -  val ctxt_args: (ProofContext.context -> method) -> src -> ProofContext.context -> method
    1.78 -  val no_args: method -> src -> ProofContext.context -> method
    1.79 +    -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
    1.80 +  val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
    1.81 +  val no_args: method -> src -> Proof.context -> method
    1.82    type modifier
    1.83    val sectioned_args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.84      (Args.T list -> modifier * Args.T list) list ->
    1.85 -    ('a -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
    1.86 +    ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
    1.87    val bang_sectioned_args:
    1.88      (Args.T list -> modifier * Args.T list) list ->
    1.89 -    (thm list -> ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
    1.90 +    (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
    1.91    val bang_sectioned_args':
    1.92      (Args.T list -> modifier * Args.T list) list ->
    1.93      (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.94 -    ('a -> thm list -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
    1.95 +    ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
    1.96    val only_sectioned_args:
    1.97      (Args.T list -> modifier * Args.T list) list ->
    1.98 -    (ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
    1.99 -  val thms_ctxt_args: (thm list -> ProofContext.context -> 'a) -> src ->
   1.100 -    ProofContext.context -> 'a
   1.101 -  val thms_args: (thm list -> 'a) -> src -> ProofContext.context -> 'a
   1.102 -  val thm_args: (thm -> 'a) -> src -> ProofContext.context -> 'a
   1.103 +    (Proof.context -> 'a) -> src -> Proof.context -> 'a
   1.104 +  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src ->
   1.105 +    Proof.context -> 'a
   1.106 +  val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
   1.107 +  val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
   1.108    val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
   1.109 -    -> src -> ProofContext.context -> method
   1.110 +    -> src -> Proof.context -> method
   1.111    val goal_args': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
   1.112 -    -> ('a -> int -> tactic) -> src -> ProofContext.context -> method
   1.113 +    -> ('a -> int -> tactic) -> src -> Proof.context -> method
   1.114    val goal_args_ctxt: (Args.T list -> 'a * Args.T list) ->
   1.115 -    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
   1.116 +    (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
   1.117    val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
   1.118 -    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
   1.119 +    (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
   1.120  end;
   1.121  
   1.122  structure Method: METHOD =
   1.123 @@ -467,12 +467,12 @@
   1.124  
   1.125  (* ML tactics *)
   1.126  
   1.127 -val tactic_ref = ref ((fn _ => raise Match): ProofContext.context -> thm list -> tactic);
   1.128 +val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
   1.129  fun set_tactic f = tactic_ref := f;
   1.130  
   1.131  fun tactic txt ctxt = METHOD (fn facts =>
   1.132    (Context.use_mltext
   1.133 -    ("let fun tactic (ctxt: ProofContext.context) (facts: thm list) : tactic = \
   1.134 +    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
   1.135         \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
   1.136         \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
   1.137         ^ txt ^
   1.138 @@ -489,7 +489,7 @@
   1.139  type src = Args.src;
   1.140  
   1.141  datatype text =
   1.142 -  Basic of (ProofContext.context -> method) |
   1.143 +  Basic of (Proof.context -> method) |
   1.144    Source of src |
   1.145    Source_i of src |
   1.146    Then of text list |
   1.147 @@ -514,7 +514,7 @@
   1.148  structure MethodsData = TheoryDataFun
   1.149  (struct
   1.150    val name = "Isar/methods";
   1.151 -  type T = (((src -> ProofContext.context -> method) * string) * stamp) NameSpace.table;
   1.152 +  type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
   1.153  
   1.154    val empty = NameSpace.empty_table;
   1.155    val copy = I;
   1.156 @@ -577,7 +577,7 @@
   1.157    Context.use_let
   1.158      "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
   1.159      \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
   1.160 -    \val method: bstring * (Method.src -> ProofContext.context -> Proof.method) * string"
   1.161 +    \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
   1.162      "Method.add_method method"
   1.163      ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
   1.164  
   1.165 @@ -592,7 +592,7 @@
   1.166  fun simple_args scan f src ctxt : method =
   1.167    #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
   1.168  
   1.169 -fun ctxt_args (f: ProofContext.context -> method) src ctxt =
   1.170 +fun ctxt_args (f: Proof.context -> method) src ctxt =
   1.171    #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
   1.172  
   1.173  fun no_args m = ctxt_args (K m);
   1.174 @@ -600,7 +600,7 @@
   1.175  
   1.176  (* sections *)
   1.177  
   1.178 -type modifier = (ProofContext.context -> ProofContext.context) * attribute;
   1.179 +type modifier = (Proof.context -> Proof.context) * attribute;
   1.180  
   1.181  local
   1.182  
   1.183 @@ -643,7 +643,7 @@
   1.184  
   1.185  fun modifier name kind kind' att =
   1.186    Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME)
   1.187 -    >> (pair (I: ProofContext.context -> ProofContext.context) o att);
   1.188 +    >> (pair (I: Proof.context -> Proof.context) o att);
   1.189  
   1.190  val iprover_modifiers =
   1.191   [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,