Very good! This is very convenient.
On 01/06/16 21:42, Makarius wrote:
*** ML ***
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing.
Florian has already hinted at it, but I will say it again explicitly:
Mathematically, gcd and lcm are not operations on the elements of a
ring, but on the equivalence classes w.r.t. associatedness (i.e. mutual
divisibility). In fact, these equivalence classes form a complete
lattice w.r.t.
I believe Florian's proposal is good. On a proof-engineering level, the
only "inconvinience" is mainly that the property
gcd a b * lcm a b = a * b
does not hold as such but generally I suspect in the form
gcd a b * lcm a b = normalize(a * b) -- The normalize in GCD.thy perhaps
has the property
Hi Developer,
my interest is to guess list operation and surface operation in many valued
logic
however, there is no result when search artificial intelligence to guess
list operation.
then i found that Isabelle can derive list operation with Lemma,
I have created 3 valued logic, however, i
