Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bind_thm;
authorwenzelm
Wed, 01 Sep 1999 21:21:22 +0200
changeset 7422 c63d619286a3
parent 7421 0577bb18b1ab
child 7423 28b48fcb0d55
bind_thm;
src/FOL/FOL_lemmas1.ML file | annotate | diff | comparison | revisions
src/FOL/IFOL_lemmas.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/FOL_lemmas1.ML	Wed Sep 01 21:21:01 1999 +0200
+++ b/src/FOL/FOL_lemmas1.ML	Wed Sep 01 21:21:22 1999 +0200
@@ -7,7 +7,7 @@
 *)
 
 val classical = thm "classical";
-val ccontr = FalseE RS classical;
+bind_thm ("ccontr", FalseE RS classical);
 
 
 (*** Classical introduction rules for | and EX ***)
--- a/src/FOL/IFOL_lemmas.ML	Wed Sep 01 21:21:01 1999 +0200
+++ b/src/FOL/IFOL_lemmas.ML	Wed Sep 01 21:21:22 1999 +0200
@@ -251,7 +251,7 @@
  (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]);
 
 (** ~ b=a ==> ~ a=b **)
-val [not_sym] = compose(sym,2,contrapos);
+bind_thm ("not_sym", hd (compose(sym,2,contrapos)));
 
 
 (* Two theorms for rewriting only one instance of a definition:
@@ -358,7 +358,7 @@
                (explode"PQRS"));
 
 (*special case for the equality predicate!*)
-val eq_cong = read_instantiate [("P","op =")] pred2_cong;
+bind_thm ("eq_cong", read_instantiate [("P","op =")] pred2_cong);
 
 
 (*** Simplifications of assumed implications.
isabelle