Locales don't work

9 views
Skip to first unread message

Victor Porton

unread,
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

Slawomir Kolodynski

unread,
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)"

lemma mylemma: shows "1 = 1" by simp;

end


--- On Fri, 3/6/09, Victor Porton <por...@narod.ru> wrote:
Reply all
Reply to author
Forward
0 new messages