Locales don't work
11 views
Skip to first unread message
Victor Porton
Mar 6, 2009, 3:00:48 PM3/6/09
to vdash
I am trying to add a new theorem (my first theorem BTW).
Proof General says:
*** Outer syntax error: keyword "is" expected,
*** but identifier small was found
Where is the error?
theory embedding
imports ZF
begin
locale embedding =
fixes big and small and embed
assumes is_inj: embded \<in> inj(small, big)
begin
lemma "1 = 1" by simp
end
end
Proof General says:
*** Outer syntax error: keyword "is" expected,
*** but identifier small was found
Where is the error?
theory embedding
imports ZF
begin
locale embedding =
fixes big and small and embed
assumes is_inj: embded \<in> inj(small, big)
begin
lemma "1 = 1" by simp
end
end
Slawomir Kolodynski
Mar 6, 2009, 6:20:55 PM3/6/09
to vd...@googlegroups.com
You want something like this:
theory embedding
imports Nat_ZF
begin
locale embedding =
fixes big and small and embed
assumes is_inj: "embded \<in> inj(small, big)"
end
--- On Fri, 3/6/09, Victor Porton <por...@narod.ru> wrote:
Reply all
Reply to author
Forward
0 new messages