1.1 --- a/doc-src/IsarRef/Thy/Spec.thy Wed Sep 08 10:45:55 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Wed Sep 08 13:22:24 2010 +0200
1.3 @@ -1069,7 +1069,6 @@
1.4 \begin{matharray}{rcl}
1.5 @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
1.6 @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
1.7 - @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
1.8 \end{matharray}
1.9
1.10 \begin{rail}
1.11 @@ -1079,18 +1078,6 @@
1.12 ;
1.13 \end{rail}
1.14
1.15 - \begin{rail}
1.16 - 'constdefs' structs? (constdecl? constdef +)
1.17 - ;
1.18 -
1.19 - structs: '(' 'structure' (vars + 'and') ')'
1.20 - ;
1.21 - constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1.22 - ;
1.23 - constdef: thmdecl? prop
1.24 - ;
1.25 - \end{rail}
1.26 -
1.27 \begin{description}
1.28
1.29 \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
1.30 @@ -1111,25 +1098,6 @@
1.31 message would be issued for any definitional equation with a more
1.32 special type than that of the corresponding constant declaration.
1.33
1.34 - \item @{command "constdefs"} combines constant declarations and
1.35 - definitions, with type-inference taking care of the most general
1.36 - typing of the given specification (the optional type constraint may
1.37 - refer to type-inference dummies ``@{text _}'' as usual). The
1.38 - resulting type declaration needs to agree with that of the
1.39 - specification; overloading is \emph{not} supported here!
1.40 -
1.41 - The constant name may be omitted altogether, if neither type nor
1.42 - syntax declarations are given. The canonical name of the
1.43 - definitional axiom for constant @{text c} will be @{text c_def},
1.44 - unless specified otherwise. Also note that the given list of
1.45 - specifications is processed in a strictly sequential manner, with
1.46 - type-checking being performed independently.
1.47 -
1.48 - An optional initial context of @{text "(structure)"} declarations
1.49 - admits use of indexed syntax, using the special symbol @{verbatim
1.50 - "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
1.51 - particularly useful with locales (see also \secref{sec:locale}).
1.52 -
1.53 \end{description}
1.54 *}
1.55
2.1 --- a/src/Pure/IsaMakefile Wed Sep 08 10:45:55 2010 +0200
2.2 +++ b/src/Pure/IsaMakefile Wed Sep 08 13:22:24 2010 +0200
2.3 @@ -112,7 +112,6 @@
2.4 Isar/class.ML \
2.5 Isar/class_declaration.ML \
2.6 Isar/code.ML \
2.7 - Isar/constdefs.ML \
2.8 Isar/context_rules.ML \
2.9 Isar/element.ML \
2.10 Isar/expression.ML \
3.1 --- a/src/Pure/Isar/constdefs.ML Wed Sep 08 10:45:55 2010 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,73 +0,0 @@
3.4 -(* Title: Pure/Isar/constdefs.ML
3.5 - Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
3.6 -
3.7 -Old-style constant definitions, with type-inference and optional
3.8 -structure context; specifications need to observe strictly sequential
3.9 -dependencies; no support for overloading.
3.10 -*)
3.11 -
3.12 -signature CONSTDEFS =
3.13 -sig
3.14 - val add_constdefs: (binding * string option) list *
3.15 - ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory
3.16 - val add_constdefs_i: (binding * typ option) list *
3.17 - ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory
3.18 -end;
3.19 -
3.20 -structure Constdefs: CONSTDEFS =
3.21 -struct
3.22 -
3.23 -(** add_constdefs(_i) **)
3.24 -
3.25 -fun gen_constdef prep_vars prep_prop prep_att
3.26 - structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
3.27 - let
3.28 - val _ = legacy_feature "Old 'constdefs' command -- use 'definition' instead";
3.29 -
3.30 - fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
3.31 -
3.32 - val thy_ctxt = ProofContext.init_global thy;
3.33 - val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
3.34 - val ((d, mx), var_ctxt) =
3.35 - (case raw_decl of
3.36 - NONE => ((NONE, NoSyn), struct_ctxt)
3.37 - | SOME raw_var =>
3.38 - struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
3.39 - ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
3.40 -
3.41 - val prop = prep_prop var_ctxt raw_prop;
3.42 - val (c, T) = #1 (Local_Defs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
3.43 - val _ =
3.44 - (case Option.map Name.of_binding d of
3.45 - NONE => ()
3.46 - | SOME c' =>
3.47 - if c <> c' then
3.48 - err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
3.49 - else ());
3.50 - val b = Binding.name c;
3.51 -
3.52 - val head = Const (Sign.full_bname thy c, T);
3.53 - val def = Term.subst_atomic [(Free (c, T), head)] prop;
3.54 - val name = Thm.def_binding_optional b raw_name;
3.55 - val atts = map (prep_att thy) raw_atts;
3.56 -
3.57 - val thy' =
3.58 - thy
3.59 - |> Sign.add_consts_i [(b, T, mx)]
3.60 - |> PureThy.add_defs false [((name, def), atts)]
3.61 - |-> (fn [thm] => (* FIXME thm vs. atts !? *)
3.62 - Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #>
3.63 - Code.add_default_eqn thm);
3.64 - in ((c, T), thy') end;
3.65 -
3.66 -fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
3.67 - let
3.68 - val ctxt = ProofContext.init_global thy;
3.69 - val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
3.70 - val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
3.71 - in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
3.72 -
3.73 -val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
3.74 -val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
3.75 -
3.76 -end;
4.1 --- a/src/Pure/Isar/isar_syn.ML Wed Sep 08 10:45:55 2010 +0200
4.2 +++ b/src/Pure/Isar/isar_syn.ML Wed Sep 08 13:22:24 2010 +0200
4.3 @@ -203,25 +203,6 @@
4.4 >> (Toplevel.theory o Isar_Cmd.add_defs));
4.5
4.6
4.7 -(* old constdefs *)
4.8 -
4.9 -val old_constdecl =
4.10 - Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) ||
4.11 - Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix'
4.12 - --| Scan.option Parse.where_ >> Parse.triple1 ||
4.13 - Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
4.14 -
4.15 -val old_constdef = Scan.option old_constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop);
4.16 -
4.17 -val structs =
4.18 - Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
4.19 - |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) [];
4.20 -
4.21 -val _ =
4.22 - Outer_Syntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
4.23 - (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
4.24 -
4.25 -
4.26 (* constant definitions and abbreviations *)
4.27
4.28 val _ =
5.1 --- a/src/Pure/ROOT.ML Wed Sep 08 10:45:55 2010 +0200
5.2 +++ b/src/Pure/ROOT.ML Wed Sep 08 13:22:24 2010 +0200
5.3 @@ -226,7 +226,6 @@
5.4 use "Isar/spec_rules.ML";
5.5 use "Isar/specification.ML";
5.6 use "Isar/typedecl.ML";
5.7 -use "Isar/constdefs.ML";
5.8
5.9 (*toplevel transactions*)
5.10 use "Thy/thy_load.ML";