adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Removed unused "Noting"

This commit is contained in:
Daniel Matichuk 2015-07-08 17:05:19 +10:00
parent 12a3fd829b
commit 5c6a3371c4
1 changed files with 0 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
lib/subgoal_focus/Noting.thy
View File

@ -1,31 +0,0 @@
(* Backwards version of "note" command. Most applicable within a subgoal focus.*)
theory Noting
imports Pure
keywords "noting" :: prf_decl
begin
ML\<open>
local
fun gen_thmss prep_atts prep_fact args state =
state
|> Proof.map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
(Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
|> snd;
in
val noting_thmss = gen_thmss (K I) (K I);
val noting_thmss_cmd = gen_thmss Attrib.attribute_cmd Proof_Context.get_fact;
end
val _ =
Outer_Syntax.command @{command_keyword noting} "define facts"
(Parse_Spec.name_facts >> (Toplevel.proof o noting_thmss_cmd));
\<close>
end