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

src/HOL/HOL.ML

changeset 3621 | d3e248853428 |

parent 3615 | e5322197cfea |

child 3646 | a11338a5d2d4 |

--- a/src/HOL/HOL.ML Wed Aug 06 11:56:31 1997 +0200 +++ b/src/HOL/HOL.ML Wed Aug 06 11:57:20 1997 +0200 @@ -349,14 +349,11 @@ _ $ (Const("op -->",_)$_$_) => th RS mp | _ => raise THM("RSmp",0,[th])); -(*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 in trans funs end; -end; - fun qed_spec_mp name = let val thm = normalize_thm [RSspec,RSmp] (result()) in bind_thm(name, thm) end; @@ -367,6 +364,9 @@ fun qed_goalw_spec_mp name thy defs s p = bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p)); +end; + + (*Thus, assignments to the references claset and simpset are recorded with theory "HOL". These files cannot be loaded directly in ROOT.ML.*) use "hologic.ML";