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.
added lemma fresh_right, which is useful
authorurbanc
Wed, 03 May 2006 02:16:23 +0200
changeset 19548 c0a896828194
parent 19547 17f504343d0f
child 19549 a8ed346f8635
added lemma fresh_right, which is useful in the proof of the recursion combinator
src/HOL/Nominal/nominal_atoms.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue May 02 20:42:43 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed May 03 02:16:23 2006 +0200
@@ -672,6 +672,8 @@
        val dj_supp             = thm "Nominal.dj_supp";
        val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
        val fresh_left          = thm "Nominal.pt_fresh_left";
+       val fresh_right_ineq    = thm "Nominal.pt_fresh_right_ineq";
+       val fresh_right         = thm "Nominal.pt_fresh_right";
        val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
        val fresh_bij           = thm "Nominal.pt_fresh_bij";
        val pt_pi_rev           = thm "Nominal.pt_pi_rev";
@@ -780,6 +782,10 @@
 		  and thms2 = inst_pt_pt_at_cp [fresh_left_ineq]
 	      in [(("fresh_left", thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss
+	      let val thms1 = inst_pt_at [fresh_right]
+		  and thms2 = inst_pt_pt_at_cp [fresh_right_ineq]
+	      in [(("fresh_right", thms1 @ thms2),[])] end
+            ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_bij]
 		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
 	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
isabelle