summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/HOL.ML

changeset 3615 | e5322197cfea |

parent 3436 | d68dbb8f22d3 |

child 3621 | d3e248853428 |

--- a/src/HOL/HOL.ML Wed Aug 06 01:12:03 1997 +0200 +++ b/src/HOL/HOL.ML Wed Aug 06 01:13:46 1997 +0200 @@ -349,7 +349,7 @@ _ $ (Const("op -->",_)$_$_) => th RS mp | _ => raise THM("RSmp",0,[th])); -(*Used in qed_spec_mp, etc., which are declared in thy_data.ML*) +(*Used in qed_spec_mp, etc.*) fun normalize_thm funs = let fun trans [] th = th | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th @@ -357,6 +357,15 @@ end; +fun qed_spec_mp name = + let val thm = normalize_thm [RSspec,RSmp] (result()) + in bind_thm(name, thm) end; + +fun qed_goal_spec_mp name thy s p = + bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p)); + +fun qed_goalw_spec_mp name thy defs s p = + bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p)); (*Thus, assignments to the references claset and simpset are recorded with theory "HOL". These files cannot be loaded directly in ROOT.ML.*)