tuned whitespace;
authorwenzelm
Wed May 13 17:36:33 2015 +0200 (2015-05-13)
changeset 60283c927fa99d045
parent 60282 496fa0fc91b1
child 60284 014b86186c49
tuned whitespace;
src/Pure/Isar/generic_target.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Wed May 13 17:27:12 2015 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Wed May 13 17:36:33 2015 +0200
     1.3 @@ -7,17 +7,17 @@
     1.4  
     1.5  signature GENERIC_TARGET =
     1.6  sig
     1.7 -  (* consts *)
     1.8 +  (*consts*)
     1.9    val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
    1.10      local_theory -> local_theory
    1.11  
    1.12 -  (* background operations *)
    1.13 +  (*background operations*)
    1.14    val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    1.15      term list * term list -> local_theory -> (term * thm) * local_theory
    1.16    val background_declaration: declaration -> local_theory -> local_theory
    1.17    val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
    1.18  
    1.19 -  (* lifting primitives to local theory operations *)
    1.20 +  (*lifting primitives to local theory operations*)
    1.21    val define: (((binding * typ) * mixfix) * (binding * term) ->
    1.22        term list * term list -> local_theory -> (term * thm) * local_theory) ->
    1.23      bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.24 @@ -31,7 +31,7 @@
    1.25        term list * term list -> local_theory -> local_theory) ->
    1.26      string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
    1.27  
    1.28 -  (* theory operations *)
    1.29 +  (*theory operations*)
    1.30    val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    1.31      term list * term list -> local_theory -> (term * thm) * local_theory
    1.32    val theory_notes: string ->
    1.33 @@ -44,7 +44,7 @@
    1.34    val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    1.35      local_theory -> local_theory
    1.36  
    1.37 -  (* locale operations *)
    1.38 +  (*locale operations*)
    1.39    val locale_notes: string -> string ->
    1.40      (Attrib.binding * (thm list * Token.src list) list) list ->
    1.41      (Attrib.binding * (thm list * Token.src list) list) list ->
    1.42 @@ -75,6 +75,7 @@
    1.43      else ctxt) lthy;
    1.44  
    1.45  
    1.46 +
    1.47  (** declarations **)
    1.48  
    1.49  fun standard_declaration pred decl lthy =
    1.50 @@ -84,6 +85,7 @@
    1.51      else ctxt) lthy;
    1.52  
    1.53  
    1.54 +
    1.55  (** consts **)
    1.56  
    1.57  fun check_mixfix ctxt (b, extra_tfrees) mx =
    1.58 @@ -123,7 +125,7 @@
    1.59            | _ => NONE)
    1.60          else NONE;
    1.61      in
    1.62 -      case const_alias of
    1.63 +      (case const_alias of
    1.64          SOME c =>
    1.65            context
    1.66            |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c)
    1.67 @@ -133,7 +135,7 @@
    1.68            |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
    1.69            |-> (fn (const as Const (c, _), _) => same_shape ?
    1.70                  (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
    1.71 -                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))
    1.72 +                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
    1.73      end
    1.74    else context;
    1.75  
    1.76 @@ -141,6 +143,7 @@
    1.77    standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
    1.78  
    1.79  
    1.80 +
    1.81  (** background primitives **)
    1.82  
    1.83  fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    1.84 @@ -170,6 +173,7 @@
    1.85    #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params))
    1.86  
    1.87  
    1.88 +
    1.89  (** lifting primitive to local theory operations **)
    1.90  
    1.91  (* define *)
    1.92 @@ -300,6 +304,7 @@
    1.93    end;
    1.94  
    1.95  
    1.96 +
    1.97  (** theory operations **)
    1.98  
    1.99  fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   1.100 @@ -326,6 +331,7 @@
   1.101    Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
   1.102  
   1.103  
   1.104 +
   1.105  (** locale operations **)
   1.106  
   1.107  fun locale_notes locale kind global_facts local_facts =