Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
authorwenzelm
Tue Oct 09 17:10:36 2007 +0200 (2007-10-09)
changeset 2492748e08f37ce92
parent 24926 bcb6b098df11
child 24928 3419943838f5
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
src/HOL/Tools/recdef_package.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Oct 09 17:10:34 2007 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Oct 09 17:10:36 2007 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4        error ("No termination condition #" ^ string_of_int i ^
     1.5          " in recdef definition of " ^ quote name);
     1.6    in
     1.7 -    Specification.theorem_i Thm.internalK NONE (K I) (bname, atts)
     1.8 +    Specification.theorem Thm.internalK NONE (K I) (bname, atts)
     1.9        [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    1.10    end;
    1.11  
     2.1 --- a/src/Pure/Isar/specification.ML	Tue Oct 09 17:10:34 2007 +0200
     2.2 +++ b/src/Pure/Isar/specification.ML	Tue Oct 09 17:10:36 2007 +0200
     2.3 @@ -10,49 +10,49 @@
     2.4  sig
     2.5    val quiet_mode: bool ref
     2.6    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
     2.7 -  val read_specification: (string * string option * mixfix) list ->
     2.8 -    ((string * Attrib.src list) * string list) list list -> Proof.context ->
     2.9 -    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.10 -    Proof.context
    2.11    val check_specification: (string * typ option * mixfix) list ->
    2.12      ((string * Attrib.src list) * term list) list list -> Proof.context ->
    2.13      (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.14      Proof.context
    2.15 -  val read_free_specification: (string * string option * mixfix) list ->
    2.16 -    ((string * Attrib.src list) * string list) list -> Proof.context ->
    2.17 +  val read_specification: (string * string option * mixfix) list ->
    2.18 +    ((string * Attrib.src list) * string list) list list -> Proof.context ->
    2.19      (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.20      Proof.context
    2.21    val check_free_specification: (string * typ option * mixfix) list ->
    2.22      ((string * Attrib.src list) * term list) list -> Proof.context ->
    2.23      (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.24      Proof.context
    2.25 -  val axiomatization: (string * string option * mixfix) list ->
    2.26 +  val read_free_specification: (string * string option * mixfix) list ->
    2.27 +    ((string * Attrib.src list) * string list) list -> Proof.context ->
    2.28 +    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.29 +    Proof.context
    2.30 +  val axiomatization: (string * typ option * mixfix) list ->
    2.31 +    ((bstring * Attrib.src list) * term list) list -> local_theory ->
    2.32 +    (term list * (bstring * thm list) list) * local_theory
    2.33 +  val axiomatization_cmd: (string * string option * mixfix) list ->
    2.34      ((bstring * Attrib.src list) * string list) list -> local_theory ->
    2.35      (term list * (bstring * thm list) list) * local_theory
    2.36 -  val axiomatization_i: (string * typ option * mixfix) list ->
    2.37 -    ((bstring * Attrib.src list) * term list) list -> local_theory ->
    2.38 -    (term list * (bstring * thm list) list) * local_theory
    2.39    val definition:
    2.40 -    (string * string option * mixfix) option * ((string * Attrib.src list) * string) ->
    2.41 -    local_theory -> (term * (bstring * thm)) * local_theory
    2.42 -  val definition_i:
    2.43      (string * typ option * mixfix) option * ((string * Attrib.src list) * term) ->
    2.44      local_theory -> (term * (bstring * thm)) * local_theory
    2.45 -  val abbreviation: Syntax.mode -> (string * string option * mixfix) option * string ->
    2.46 -    local_theory -> local_theory
    2.47 -  val abbreviation_i: Syntax.mode -> (string * typ option * mixfix) option * term ->
    2.48 +  val definition_cmd:
    2.49 +    (string * string option * mixfix) option * ((string * Attrib.src list) * string) ->
    2.50 +    local_theory -> (term * (bstring * thm)) * local_theory
    2.51 +  val abbreviation: Syntax.mode -> (string * typ option * mixfix) option * term ->
    2.52      local_theory -> local_theory
    2.53 -  val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    2.54 -  val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    2.55 -  val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    2.56 +  val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string ->
    2.57 +    local_theory -> local_theory
    2.58 +  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    2.59 +  val notation_cmd: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    2.60 +  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
    2.61      -> local_theory -> (bstring * thm list) list * local_theory
    2.62 -  val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
    2.63 +  val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    2.64      -> local_theory -> (bstring * thm list) list * local_theory
    2.65    val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
    2.66 -    string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
    2.67 +    string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
    2.68      bool -> local_theory -> Proof.state
    2.69 -  val theorem_i: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
    2.70 -    string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
    2.71 +  val theorem_cmd: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
    2.72 +    string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
    2.73      bool -> local_theory -> Proof.state
    2.74    val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    2.75  end;
    2.76 @@ -167,8 +167,8 @@
    2.77      val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) cs;
    2.78    in ((consts, axioms), lthy'') end;
    2.79  
    2.80 -val axiomatization = gen_axioms read_specification;
    2.81 -val axiomatization_i = gen_axioms check_specification;
    2.82 +val axiomatization = gen_axioms check_specification;
    2.83 +val axiomatization_cmd = gen_axioms read_specification;
    2.84  
    2.85  
    2.86  (* definition *)
    2.87 @@ -192,8 +192,8 @@
    2.88      val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
    2.89    in ((lhs, (b, th')), lthy3) end;
    2.90  
    2.91 -val definition = gen_def read_free_specification;
    2.92 -val definition_i = gen_def check_free_specification;
    2.93 +val definition = gen_def check_free_specification;
    2.94 +val definition_cmd = gen_def read_free_specification;
    2.95  
    2.96  
    2.97  (* abbreviation *)
    2.98 @@ -215,8 +215,8 @@
    2.99      val _ = print_consts lthy' (K false) [(x, T)]
   2.100    in lthy' end;
   2.101  
   2.102 -val abbreviation = gen_abbrev read_free_specification;
   2.103 -val abbreviation_i = gen_abbrev check_free_specification;
   2.104 +val abbreviation = gen_abbrev check_free_specification;
   2.105 +val abbreviation_cmd = gen_abbrev read_free_specification;
   2.106  
   2.107  
   2.108  (* notation *)
   2.109 @@ -224,8 +224,8 @@
   2.110  fun gen_notation prep_const mode args lthy =
   2.111    lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
   2.112  
   2.113 -val notation = gen_notation ProofContext.read_const;
   2.114 -val notation_i = gen_notation (K I);
   2.115 +val notation = gen_notation (K I);
   2.116 +val notation_cmd = gen_notation ProofContext.read_const;
   2.117  
   2.118  
   2.119  (* fact statements *)
   2.120 @@ -240,8 +240,8 @@
   2.121      val _ = present_results' lthy' kind res;
   2.122    in (res, lthy') end;
   2.123  
   2.124 -val theorems = gen_theorems ProofContext.get_thms Attrib.intern_src;
   2.125 -val theorems_i = gen_theorems (K I) (K I);
   2.126 +val theorems = gen_theorems (K I) (K I);
   2.127 +val theorems_cmd = gen_theorems ProofContext.get_thms Attrib.intern_src;
   2.128  
   2.129  
   2.130  (* complex goal statements *)
   2.131 @@ -351,8 +351,8 @@
   2.132  
   2.133  in
   2.134  
   2.135 -val theorem = gen_theorem Attrib.intern_src Locale.read_context_statement_i;
   2.136 -val theorem_i = gen_theorem (K I) Locale.cert_context_statement;
   2.137 +val theorem = gen_theorem (K I) Locale.cert_context_statement;
   2.138 +val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement_i;
   2.139  
   2.140  fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
   2.141