Permalink
Switch branches/tags
Nothing to show
Commits on Feb 11, 2013
Commits on Feb 3, 2013
Commits on Dec 14, 2012
  1. Get rid of spurious kindbind; jhilbert doesn't need it and ghilbert i…

    Jim Kingdon
    Jim Kingdon committed Dec 14, 2012
    …s pickier about rejecting it.
Commits on Nov 23, 2012
  1. Put <jh> on line by itself.

    Jim Kingdon
    Jim Kingdon committed Nov 23, 2012
Commits on Nov 21, 2012
  1. Put one more </jh> on its own line.

    Jim Kingdon
    Jim Kingdon committed Nov 21, 2012
  2. Merge branch 'levitation'

    Jim Kingdon
    Jim Kingdon committed Nov 21, 2012
    Conflicts:
    	User talk/R/a/p/Raph
    	Wikiproofs/T/e/a/Tearoom
Commits on Nov 19, 2012
  1. put <jh> and </jh> on their own line. This is the style we use elsewh…

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Nov 19, 2012
    …ere.
    
     'Main:Tutorial' (rev 2808)
  2. put <jh> and </jh> tags on their own line. This is the style we use e…

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Nov 19, 2012
    …lsewhere.
    
     'Interface:Tutorial' (rev 2807)
Commits on Nov 7, 2012
  1. Add buildAdditionLLInConsequent, RealAdditiveIdentityLeft; finish Rea…

    Jim Kingdon
    Jim Kingdon committed Nov 7, 2012
    …lZeroDifferenceEquality.
Commits on Oct 25, 2012
  1. /* bug in ghilbert, or am I just confused? */ thanks

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Oct 25, 2012
     'User talk:Raph' (rev 2803)
  2. answer to distinct var constraints.

    Raph Levitation-perl
    Raph authored and Levitation-perl committed Oct 25, 2012
     'User talk:Raph' (rev 2801)
Commits on Oct 21, 2012
  1. /* ghilbert */ new section

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Oct 21, 2012
     'Wikiproofs:Tearoom' (rev 2798)
Commits on Oct 16, 2012
  1. Add swapBiconditionalInConsequent.

    Jim Kingdon
    Jim Kingdon committed Oct 16, 2012
  2. Add closeAdditiveInverseInConsequent.

    Jim Kingdon
    Jim Kingdon committed Oct 16, 2012
Commits on Oct 12, 2012
  1. Get a start on RealZeroDifferenceEquality.

    Jim Kingdon
    Jim Kingdon committed Oct 12, 2012
  2. Add RealSubtractionItself.

    Jim Kingdon
    Jim Kingdon committed Oct 12, 2012
Commits on Oct 9, 2012
  1. Merge remote-tracking branch 'levitation/master'

    Jim Kingdon
    Jim Kingdon committed Oct 9, 2012
    Conflicts:
    	Interface/F/i/r/First-order logic with quantifiability
  2. Add RealSubtractionItselfLemma.

    Jim Kingdon
    Jim Kingdon committed Oct 9, 2012
Commits on Oct 7, 2012
  1. Rename ClosureLemma3 to UnionUnique, as I think it will be handy for …

    Jim Kingdon
    Jim Kingdon committed Oct 7, 2012
    …more than proving Closure.
Commits on Oct 6, 2012
  1. Add RealSubtraction.

    Jim Kingdon
    Jim Kingdon committed Oct 6, 2012
  2. Add buildAddition and other convenience builders.

    Jim Kingdon
    Jim Kingdon committed Oct 6, 2012
  3. finish this, and export the result

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Oct 6, 2012
     'Main:Real numbers as a subset of complex numbers' (rev 2797)
  4. rename Reciprocal to RealReciprocal, in accordance with the general n…

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Oct 6, 2012
    …aming convention
    
     'Interface:Real numbers' (rev 2796)
  5. add theorems for the realness of various constants

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Oct 6, 2012
     'Interface:Real numbers' (rev 2795)
  6. Remove conflict markers which somehow got checked in.

    Jim Kingdon
    Jim Kingdon committed Oct 6, 2012
Commits on Oct 5, 2012
  1. fix copy-paste error where we refer to the wrong variable; not too su…

    Kingdon Levitation-perl
    Kingdon authored and Levitation-perl committed Oct 5, 2012
    …re one way or the other about the distinct variable constraint
    
     'Interface:First-order logic with quantifiability' (rev 2794)
  2. We'd like to call it RealSubtractionClosure not RealSubtractionClosed…

    Jim Kingdon
    Jim Kingdon committed Oct 5, 2012
    …. Take a baby step in that direction.
  3. Add RealAdditiveInverseClosed.

    Jim Kingdon
    Jim Kingdon committed Oct 5, 2012
Commits on Oct 4, 2012
  1. Prove RealAdditiveInverseClosed-uniq2.

    Jim Kingdon
    Jim Kingdon committed Oct 4, 2012
Commits on Oct 2, 2012
  1. Sketch proof of RealAdditiveInverseClosed-uniq2.

    Jim Kingdon
    Jim Kingdon committed Oct 2, 2012
  2. Merge remote-tracking branch 'levitation/master'

    Jim Kingdon
    Jim Kingdon committed Oct 2, 2012
    Conflicts:
    	Interface/F/i/r/First-order linear order from strict inequality
    	Main/F/i/r/First-order linear order defined via strict inequality
    	Main/R/e/a/Real numbers
Commits on Oct 1, 2012
  1. Add RealAdditiveInverseClosed-uniq1.

    Jim Kingdon
    Jim Kingdon committed Oct 1, 2012
Commits on Sep 30, 2012
  1. Add RealAdditionCancellationLeft.

    Jim Kingdon
    Jim Kingdon committed Sep 30, 2012