--- a/NEWS Wed Mar 04 19:21:56 2009 +0000
+++ b/NEWS Wed Mar 04 19:22:32 2009 +0000
@@ -501,7 +501,7 @@
Suc_not_Zero Zero_not_Suc ~> nat.distinct
* The option datatype has been moved to a new theory HOL/Option.thy.
-Renamed option_map to Option.map.
+Renamed option_map to Option.map, and o2s to Option.set.
* Library/Nat_Infinity: added addition, numeral syntax and more
instantiations for algebraic structures. Removed some duplicate
--- a/src/HOL/HOL.thy Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/HOL.thy Wed Mar 04 19:22:32 2009 +0000
@@ -1709,6 +1709,11 @@
subsection {* Nitpick theorem store *}
ML {*
+structure Nitpick_Const_Def_Thms = NamedThmsFun
+(
+ val name = "nitpick_const_def"
+ val description = "alternative definitions of constants as needed by Nitpick"
+)
structure Nitpick_Const_Simp_Thms = NamedThmsFun
(
val name = "nitpick_const_simp"
@@ -1725,7 +1730,8 @@
val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
)
*}
-setup {* Nitpick_Const_Simp_Thms.setup
+setup {* Nitpick_Const_Def_Thms.setup
+ #> Nitpick_Const_Simp_Thms.setup
#> Nitpick_Const_Psimp_Thms.setup
#> Nitpick_Ind_Intro_Thms.setup *}
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Mar 04 19:22:32 2009 +0000
@@ -374,7 +374,9 @@
in
lthy''
|> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
- [Attrib.internal (K Simplifier.simp_add)]), maps snd simps')
+ map (Attrib.internal o K)
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
+ maps snd simps')
|> snd
end)
[goals] |>
--- a/src/HOL/Statespace/state_space.ML Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/Statespace/state_space.ML Wed Mar 04 19:22:32 2009 +0000
@@ -611,7 +611,7 @@
Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s
| NONE =>
if get_silent (Context.Proof ctxt)
- then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s
+ then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s
else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
@@ -637,8 +637,8 @@
| NONE =>
if get_silent (Context.Proof ctxt)
then Syntax.const "StateFun.update"$
- Syntax.const "arbitrary"$Syntax.const "arbitrary"$
- Syntax.free n$(Syntax.const KN $ v)$s
+ Syntax.const "undefined" $ Syntax.const "undefined" $
+ Syntax.free n $ (Syntax.const KN $ v) $ s
else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
end;
--- a/src/HOL/Tools/datatype_package.ML Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/Tools/datatype_package.ML Wed Mar 04 19:22:32 2009 +0000
@@ -629,14 +629,6 @@
(** a datatype antiquotation **)
-local
-
-val sym_datatype = Pretty.command "datatype";
-val sym_binder = Pretty.str "\\ {\\isacharequal}"; (*FIXME use proper symbol*)
-val sym_sep = Pretty.str "{\\isacharbar}\\ ";
-
-in
-
fun args_datatype (ctxt, args) =
let
val (tyco, (ctxt', args')) = Args.tyname (ctxt, args);
@@ -654,26 +646,19 @@
in if member (op =) s " " then Pretty.enclose "(" ")" [p]
else p
end;
- fun pretty_constr (co, []) =
- Syntax.pretty_term ctxt (Const (co, ty))
- | pretty_constr (co, [ty']) =
- (Pretty.block o Pretty.breaks)
- [Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
- pretty_typ_br ty']
- | pretty_constr (co, tys) =
- (Pretty.block o Pretty.breaks)
- (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_br tys);
+ fun pretty_constr (co, tys) =
+ (Pretty.block o Pretty.breaks)
+ (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
+ map pretty_typ_br tys);
in
Pretty.block
- (sym_datatype :: Pretty.brk 1 ::
+ (Pretty.command "datatype" :: Pretty.brk 1 ::
Syntax.pretty_typ ctxt ty ::
- sym_binder :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, sym_sep]
+ Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "]
(map (single o pretty_constr) cos)))
end
-end;
(** package setup **)