Interpretation equations may have name and/or attribute.
authorballarin
Fri Oct 19 12:21:32 2007 +0200 (2007-10-19)
changeset 25094ba43514068fd
parent 25093 41ec22a00c41
child 25095 ea8307dac208
Interpretation equations may have name and/or attribute.
doc-src/IsarRef/generic.tex
src/Pure/Isar/class.ML
src/Pure/Isar/spec_parse.ML
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Oct 19 10:44:45 2007 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Oct 19 12:21:32 2007 +0200
     1.3 @@ -394,8 +394,10 @@
     1.4    ;
     1.5    printinterps '!'? name
     1.6    ;
     1.7 -  interp: thmdecl? \\ (contextexpr ('[' (inst+) ']')? |
     1.8 -    name ('[' (inst+) ']')? 'where' (prop + 'and'))
     1.9 +  instantiation: ('[' (inst+) ']')?
    1.10 +  ;
    1.11 +  interp: thmdecl? \\ (contextexpr instantiation |
    1.12 +    name instantiation 'where' (thmdecl? prop + 'and'))
    1.13    ;
    1.14  \end{rail}
    1.15  
     2.1 --- a/src/Pure/Isar/class.ML	Fri Oct 19 10:44:45 2007 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 19 12:21:32 2007 +0200
     2.3 @@ -520,7 +520,8 @@
     2.4    in
     2.5      thy
     2.6      |> fold_map (get_remove_global_constraint o fst o snd) params
     2.7 -    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) (inst, defs)
     2.8 +    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
     2.9 +          (inst, map (fn def => (("", []), def)) defs)
    2.10      |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
    2.11    end;
    2.12  
     3.1 --- a/src/Pure/Isar/spec_parse.ML	Fri Oct 19 10:44:45 2007 +0200
     3.2 +++ b/src/Pure/Isar/spec_parse.ML	Fri Oct 19 12:21:32 2007 +0200
     3.3 @@ -23,7 +23,8 @@
     3.4      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
     3.5    val locale_mixfix: token list -> mixfix * token list
     3.6    val locale_fixes: token list -> (string * string option * mixfix) list * token list
     3.7 -  val locale_insts: token list -> (string option list * string list) * token list
     3.8 +  val locale_insts: token list ->
     3.9 +    (string option list * ((bstring * Attrib.src list) * string) list) * token list
    3.10    val class_expr: token list -> string list * token list
    3.11    val locale_expr: token list -> Locale.expr * token list
    3.12    val locale_keyword: token list -> string * token list
    3.13 @@ -88,7 +89,7 @@
    3.14  
    3.15  val locale_insts =
    3.16    Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    3.17 -  -- Scan.optional (P.$$$ "where" |-- P.and_list1 P.term) [];
    3.18 +  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    3.19  
    3.20  local
    3.21