Mercurial Mercurial > hg > nominal2 / 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.
LamEx.thy
changeset 218 df05cd030d2f
parent 203 7384115df9fd
child 219 329111e1c4ba 
--- a/LamEx.thy	Wed Oct 28 10:29:00 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 15:25:11 2009 +0100
@@ -23,11 +23,15 @@
 print_quotients
 
 local_setup {*
-  make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
+  old_make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
+  old_make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
+  old_make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
 *}
 
+thm Var_def
+thm App_def
+thm Lam_def
+
 lemma real_alpha:
   assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
   shows "Lam a t = Lam b s"
nominal2