Mercurial Mercurial > repos > isabelle / 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.
src/Pure/logic.ML
changeset 26424 a6cad32a27b0
parent 25939 ddea202704b4
child 27334 3f17273766f2 
--- a/src/Pure/logic.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/logic.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -145,7 +145,7 @@
 (** conjunction **)
 
 val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
-val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
+val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
 
 
 (*A && B*)
@@ -161,7 +161,7 @@
 
 
 (*A && B*)
-fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
+fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
 
 (*A && B && C -- improper*)
@@ -264,9 +264,9 @@
   | unprotect t = raise TERM ("unprotect", [t]);
 
 
-fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
+fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
 
-fun dest_term (Const ("ProtoPure.term", _) $ t) = t
+fun dest_term (Const ("Pure.term", _) $ t) = t
   | dest_term t = raise TERM ("dest_term", [t]);
isabelle