Mercurial Mercurial > repos > Old_HOL / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ex/Puzzle.ML
changeset 199 ad45e477926c
parent 171 16c4ea954511 
--- a/ex/Puzzle.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/ex/Puzzle.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -23,7 +23,7 @@
 by (subgoal_tac "f(na) <= f(f(na))" 1);
 by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
 by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1);
-val lemma = store_thm("lemma", result() RS spec RS mp);
+bind_thm("lemma", result() RS spec RS mp);
 
 goal Puzzle.thy "n <= f(n)";
 by (fast_tac (HOL_cs addIs [lemma]) 1);
@@ -38,7 +38,7 @@
 by (simp_tac nat_ss 1);
 by (simp_tac nat_ss 1);
 by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
-val mono_lemma1 = store_thm("mono_lemma1", result() RS mp);
+bind_thm("mono_lemma1", result() RS mp);
 
 val [p1,p2] = goal Puzzle.thy
     "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";
Old_HOL