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.
renamed assert_prop to ensure_prop;
authorwenzelm
Tue, 08 Nov 2005 10:43:12 +0100
changeset 18121 77b6d06ad99d
parent 18120 41328805d4db
child 18122 d5a876195499
renamed assert_prop to ensure_prop;
src/Pure/Isar/object_logic.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/object_logic.ML	Tue Nov 08 10:43:11 2005 +0100
+++ b/src/Pure/Isar/object_logic.ML	Tue Nov 08 10:43:12 2005 +0100
@@ -13,7 +13,7 @@
   val is_judgment: theory -> term -> bool
   val drop_judgment: theory -> term -> term
   val fixed_judgment: theory -> string -> term
-  val assert_propT: theory -> term -> term
+  val ensure_propT: theory -> term -> term
   val declare_atomize: theory attribute
   val declare_rulify: theory attribute
   val atomize_term: theory -> term -> term
@@ -110,7 +110,7 @@
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;
 
-fun assert_propT thy t =
+fun ensure_propT thy t =
   let val T = Term.fastype_of t
   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
isabelle