--- a/doc-src/Codegen/Thy/Further.thy Mon Sep 20 16:05:25 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Mon Sep 20 18:28:29 2010 +0200
@@ -103,7 +103,7 @@
interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
"power.powers (\<lambda>n f. f ^^ n) = funpows"
by unfold_locales
- (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
+ (simp_all add: fun_eq_iff funpow_mult mult_commute funpows_def)
text {*
\noindent This additional equation is trivially proved by the definition
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Sep 20 16:05:25 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Mon Sep 20 18:28:29 2010 +0200
@@ -191,7 +191,7 @@
\ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\isanewline
-\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
+\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fun{\isacharunderscore}eq{\isacharunderscore}iff\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 20 16:05:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 20 18:28:29 2010 +0200
@@ -34,9 +34,6 @@
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
| _ => th
-(*To enforce single-threading*)
-exception Clausify_failure of theory;
-
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 20 16:05:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 20 18:28:29 2010 +0200
@@ -138,7 +138,8 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-val preproc_ss = HOL_basic_ss addsimps @{thms all_simps [symmetric]}
+val preproc_ss =
+ HOL_basic_ss addsimps @{thms all_simps[symmetric] ex_simps[symmetric]}
fun generic_metis_tac mode ctxt ths i st0 =
let
@@ -149,13 +150,12 @@
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
Tactical.SOLVED'
- ((TRY o Simplifier.simp_tac preproc_ss)
- THEN'
- (REPEAT_DETERM o match_tac @{thms allI})
- THEN'
- TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
- (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
- ctxt) i st0
+ ((TRY o Simplifier.full_simp_tac preproc_ss)
+ THEN' (REPEAT_DETERM o match_tac @{thms allI})
+ THEN' (REPEAT_DETERM o ematch_tac @{thms exE})
+ THEN' (TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
+ (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+ ctxt)) i st0
end
val metis_tac = generic_metis_tac HO
--- a/src/Tools/Code/code_printer.ML Mon Sep 20 16:05:25 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Mon Sep 20 18:28:29 2010 +0200
@@ -130,32 +130,30 @@
fun markup_stmt name = Print_Mode.setmp [code_presentationN]
(Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
-fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
- implode (map (filter_presentation presentation_names
- (selected orelse (name = code_presentationN
- andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
- | filter_presentation presentation_names selected (XML.Text s) =
- if selected then s else "";
-
-fun maps_string s f [] = ""
- | maps_string s f (x :: xs) =
+fun filter_presentation [] tree =
+ Buffer.empty
+ |> fold XML.add_content tree
+ |> Buffer.add "\n"
+ | filter_presentation presentation_names tree =
let
- val s1 = f x;
- val s2 = maps_string s f xs;
- in if s1 = "" then s2
- else if s2 = "" then s1
- else s1 ^ s ^ s2
- end;
-
-fun plain_text (XML.Elem (_, xs)) = maps_string "" plain_text xs
- | plain_text (XML.Text s) = s
+ fun is_selected (name, attrs) =
+ name = code_presentationN
+ andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
+ fun add_content_with_space tree (is_first, buf) =
+ buf
+ |> not is_first ? Buffer.add "\n\n"
+ |> XML.add_content tree
+ |> pair false;
+ fun filter (XML.Elem (name_attrs, xs)) =
+ fold (if is_selected name_attrs then add_content_with_space else filter) xs
+ | filter (XML.Text s) = I;
+ in snd (fold filter tree (true, Buffer.empty)) end;
fun format presentation_names width =
Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
#> YXML.parse_body
- #> (if null presentation_names then maps_string "" plain_text
- else maps_string "\n\n" (filter_presentation presentation_names false))
- #> suffix "\n";
+ #> filter_presentation presentation_names
+ #> Buffer.content;
(** names and variable name contexts **)