Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle



Hi
 
as it return the fact name, I would like to know the fact body
I have search search fact in help but can not find relevant information. How to show the fact body?
 
for example rotate, body is (length xs) (xs++ys) == ys++xs
rotate (length xs) (xs++ys) == ys++xs
 
 
$ hipspec Rotate.hs --auto --cg --verbosity=30
Depth 1: 11 terms, 5 tests, 29 evaluations, 11 classes, 0 raw equations.
Depth 2: 63 terms, 100 tests, 2151 evaluations, 48 classes, 15 raw equations.
Depth 3: 1688 terms, 100 tests, 63851 evaluations, 1303 classes, 385 raw equations.
Proved xs++[] == xs by induction on xs using Z3
Proved (xs++ys)++zs == xs++(ys++zs) by induction on xs using Z3
Proved length (xs++ys) == length (ys++xs) by induction on ys,xs using Z3
Proved rotate m [] == [] without induction using Z3
Proved rotate m (rotate n xs) == rotate n (rotate m xs) by induction on n,m using Z3
Proved rotate (S m) (rotate n xs) == rotate (S n) (rotate m xs) by induction on xs using Z3
Proved rotate m (x:[]) == x:[] by induction on m using Z3
Proved rotate m xs++rotate m xs == rotate m (xs++xs) by induction on m using Z3
Proved length (rotate m xs) == length xs by induction on m using Z3
Proved rotate (length xs) (xs++ys) == ys++xs by induction on xs using Z3
Proved prop_rotate {- rotate (length xs) xs == xs -} without induction using Z3
Proved:
    xs++[] == xs
    (xs++ys)++zs == xs++(ys++zs)
    length (xs++ys) == length (ys++xs)
    rotate m (rotate n xs) == rotate n (rotate m xs)
    rotate (S m) (rotate n xs) == rotate (S n) (rotate m xs)
    rotate m (x:[]) == x:[]
    rotate m xs++rotate m xs == rotate m (xs++xs)
    length (rotate m xs) == length xs
    rotate (length xs) (xs++ys) == ys++xs
    prop_rotate {- rotate (length xs) xs == xs -}

 
Regards,
 
Martin
 
> Date: Mon, 27 Oct 2014 20:08:50 +0100
> From: makarius at sketis.net
> To: tesleft at hotmail.com
> CC: isabelle-users at cl.cam.ac.uk
> Subject: Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle
> 
> On Tue, 28 Oct 2014, M A wrote:
> 
> > http://fa.isabelle.narkive.com/LVdvCYnK/isabelle-stuck-on-proof
> >
> > above link mention in proof general, the "Isabelle/Show me .../Facts" menu
> 
> The proper spelling is "Proof General" with capitals.  It was once the 
> main user interface for Isabelle, and is still used in some other proof 
> assistants like Coq.
> 
> In Isabelle2014 Proof General is no longer included, but it happens to 
> work as "optional component" as explained in the NEWS.  In the next 
> release it will be no longer there -- its deletion is scheduled for the 
> end of this week!
> 
> As a new user of Isabelle, there is no need to know what Proof General is 
> or was.  I do recommend, though, to study the Isabelle/jEdit manual, which 
> is available in the "Documentation" panel via the label "jedit".  For 
> example, it explains how to input mathematical symbols (there is more 
> than one way to do it).
> 
> 
>  	Makarius
> 
> ----------------------------------------------------------------------------
>                     http://stop-ttip.org  742,965 people so far
> ----------------------------------------------------------------------------
> 
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.