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.
IntEx.thy
changeset 489 2b7b349e470f
parent 485 4efb104514f7
child 493 672b94510e7d 
--- a/IntEx.thy	Wed Dec 02 23:11:50 2009 +0100
+++ b/IntEx.thy	Wed Dec 02 23:31:30 2009 +0100
@@ -140,10 +140,10 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 ML {* val consts = lookup_quot_consts defs *}
 
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] defs *}
 
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
 
 
 lemma "PLUS a b = PLUS b a"
@@ -252,7 +252,7 @@
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
-apply (induct_tac xb yb rule:list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
+apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
 sorry
 
 lemma nil_listrel_rsp[quot_rsp]:
nominal2