Mercurial Mercurial > hg > nominal2 / 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.
used prop_of to get the term of a theorem (replaces crep_thm)
authorChristian Urban <urbanc@in.tum.de>
Mon, 05 Oct 2009 11:24:32 +0200
changeset 62 58384c90a5e5
parent 61 1585a60b076d
child 63 980c95c2bf7f
used prop_of to get the term of a theorem (replaces crep_thm)
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/QuotMain.thy	Fri Oct 02 11:10:21 2009 +0200
+++ b/QuotMain.thy	Mon Oct 05 11:24:32 2009 +0200
@@ -1194,7 +1194,7 @@
 
 thm leqi4_lift
 ML {*
-  val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) []))
+  val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
   val (_, l) = dest_Type typ
   val t = Type ("QuotMain.fset", l)
   val v = Var (nam, t)
@@ -1212,7 +1212,7 @@
 (*
 thm card_suc
 ML {*
-  val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) [])))
+  val (nam, typ) = hd (tl (Term.add_vars (prop_of @{thm card_suc})) [])
   val (_, l) = dest_Type typ
   val t = Type ("QuotMain.fset", l)
   val v = Var (nam, t)
nominal2