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.
Nominal/Nominal2_Base.thy
changeset 2847 5165f4552cd5
parent 2820 77e1d9f2925e
child 2848 da7e6655cd4c 
--- a/Nominal/Nominal2_Base.thy	Fri Jun 10 15:52:17 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 14 11:43:06 2011 +0100
@@ -2759,7 +2759,7 @@
   by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
 
 lemma at_base_class:
-  fixes sort_fun :: "'b \<Rightarrow>atom_sort"
+  fixes sort_fun :: "'b \<Rightarrow> atom_sort"
   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
   assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
   assumes atom_def: "\<And>a. atom a = Rep a"
nominal2