« back to all changes in this revision
Viewing changes to proof-checker-pkg.lisp
- Committer: Bazaar Package Importer
- Date: 2006-12-04 10:35:42 UTC
- mfrom: (1.1.5 upstream) (3.1.1 etch)
- Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
New upstream release
- files added:
- books/arithmetic-3/extra
- books/concurrent-programs
- books/concurrent-programs/bakery
- books/concurrent-programs/german-protocol
- books/deduction
- books/deduction/passmore
- books/defexec/other-apps
- books/defexec/other-apps/misc
- books/defexec/other-apps/qsort
- books/defexec/other-apps/records
- books/rtl/rel6
- books/rtl/rel6/arithmetic
- books/rtl/rel6/lib
- books/rtl/rel6/support
- books/rtl/rel6/support/lib1
- books/rtl/rel6/support/lib1.delta1
- books/rtl/rel6/support/support
- books/rtl/rel6/support/top
- books/rtl/rel6/user
- files removed:
- books/defexec/chapter3
- books/defexec/chapter3/misc
- books/defexec/chapter3/qsort
- books/defexec/chapter3/records
- files modified:
- GNUmakefile
- books/arithmetic-2/Makefile *
- books/arithmetic-2/README *
- books/arithmetic-2/floor-mod/Makefile *
- books/arithmetic-2/floor-mod/floor-mod-helper.lisp *
- books/arithmetic-2/floor-mod/floor-mod.lisp *
- books/arithmetic-2/meta/Makefile *
- books/arithmetic-2/meta/README *
- books/arithmetic-2/meta/cancel-terms-helper.lisp *
- books/arithmetic-2/meta/cancel-terms-meta.lisp *
- books/arithmetic-2/meta/collect-terms-meta.lisp *
- books/arithmetic-2/meta/common-meta.lisp *
- books/arithmetic-2/meta/expt-helper.lisp *
- books/arithmetic-2/meta/expt.lisp *
- books/arithmetic-2/meta/integerp-meta.lisp *
- books/arithmetic-2/meta/integerp.lisp *
- books/arithmetic-2/meta/mini-theories.lisp *
- books/arithmetic-2/meta/non-linear.lisp *
- books/arithmetic-2/meta/numerator-and-denominator.lisp *
- books/arithmetic-2/meta/post.lisp *
- books/arithmetic-2/meta/pre.lisp *
- books/arithmetic-2/meta/top.lisp *
- books/arithmetic-2/pass1/Makefile *
- books/arithmetic-2/pass1/basic-arithmetic-helper.lisp *
- books/arithmetic-2/pass1/basic-arithmetic.lisp *
- books/arithmetic-2/pass1/expt-helper.lisp *
- books/arithmetic-2/pass1/expt.lisp *
- books/arithmetic-2/pass1/inequalities.lisp *
- books/arithmetic-2/pass1/numerator-and-denominator-helper.lisp *
- books/arithmetic-2/pass1/numerator-and-denominator.lisp *
- books/arithmetic-2/pass1/prefer-times.lisp *
- books/arithmetic-2/pass1/top.lisp *
- books/arithmetic/README *
- books/arithmetic/abs.lisp *
- books/arithmetic/binomial.lisp *
- books/arithmetic/certify.lsp *
- books/arithmetic/equalities.acl2 *
- books/arithmetic/factorial.lisp *
- books/arithmetic/idiv.lisp *
- books/arithmetic/inequalities.lisp *
- books/arithmetic/mod-gcd.lisp *
- books/arithmetic/rational-listp.lisp *
- books/arithmetic/rationals.lisp *
- books/arithmetic/sumlist.lisp *
- books/arithmetic/top-with-meta.lisp *
- books/arithmetic/top.lisp *
- books/bdd/Makefile *
- books/bdd/README *
- books/bdd/alu-proofs.lisp *
- books/bdd/alu.lisp *
- books/bdd/bdd-primitives.lisp *
- books/bdd/benchmarks.acl2 *
- books/bdd/bit-vector-reader.lsp *
- books/bdd/bool-ops.lisp *
- books/bdd/certify.lsp *
- books/bdd/hamming.lisp *
- books/bdd/pg-theory.lisp *
- books/certify-numbers.lisp *
- books/cowles/Makefile *
- books/cowles/README *
- books/cowles/acl2-agp.acl2 *
- books/cowles/acl2-agp.lisp *
- books/cowles/acl2-asg.acl2 *
- books/cowles/acl2-asg.lisp *
- books/cowles/acl2-crg.acl2 *
- books/cowles/acl2-crg.lisp *
- books/cowles/certify.lsp *
- books/data-structures/Makefile *
- books/data-structures/README *
- books/data-structures/alist-defthms.lisp *
- books/data-structures/alist-defuns.lisp *
- books/data-structures/alist-theory.lisp *
- books/data-structures/array1.lisp *
- books/data-structures/certify.lsp *
- books/data-structures/defalist.acl2 *
- books/data-structures/defalist.lisp *
- books/data-structures/define-structures-package.lisp *
- books/data-structures/define-u-package.lisp *
- books/data-structures/deflist.acl2 *
- books/data-structures/list-defthms.lisp *
- books/data-structures/list-defuns.lisp *
- books/data-structures/list-theory.lisp *
- books/data-structures/memories/COPYING *
- books/data-structures/memories/Makefile *
- books/data-structures/memories/cert.acl2 *
- books/data-structures/number-list-defthms.lisp *
- books/data-structures/number-list-defuns.lisp *
- books/data-structures/number-list-theory.lisp *
- books/data-structures/set-defthms.lisp *
- books/data-structures/set-defuns.lisp *
- books/data-structures/set-theory.lisp *
- books/data-structures/structures.acl2 *
- books/data-structures/structures.lisp *
- books/data-structures/utilities.acl2 *
- books/finite-set-theory/Makefile *
- books/finite-set-theory/certify.lsp *
- books/finite-set-theory/osets/CHANGES.html *
- books/finite-set-theory/osets/COPYING *
- books/finite-set-theory/osets/Makefile *
- books/finite-set-theory/osets/README *
- books/finite-set-theory/osets/cert.acl2 *
- books/finite-set-theory/osets/computed-hints.lisp *
- books/finite-set-theory/osets/fast.lisp *
- books/finite-set-theory/osets/instance.lisp *
- books/finite-set-theory/osets/map.lisp *
- books/finite-set-theory/osets/membership.lisp *
- books/finite-set-theory/osets/outer.lisp *
- books/finite-set-theory/osets/primitives.lisp *
- books/finite-set-theory/osets/quantify.lisp *
- books/finite-set-theory/osets/set-order.lisp *
- books/finite-set-theory/osets/sets.defpkg *
- books/finite-set-theory/osets/sort.lisp *
- books/finite-set-theory/set-theory.acl2 *
- books/finite-set-theory/set-theory.lisp *
- books/finite-set-theory/total-ordering.lisp *
- books/ihs/@logops.lisp *
- books/ihs/Makefile *
- books/ihs/README *
- books/ihs/certify.lsp *
- books/ihs/ihs-definitions.lisp *
- books/ihs/ihs-init.acl2 *
- books/ihs/ihs-init.lisp *
- books/ihs/ihs-lemmas.lisp *
- books/ihs/ihs-theories.lisp *
- books/ihs/logops-definitions.lisp *
- books/ihs/math-lemmas.lisp *
- books/ihs/quotient-remainder-lemmas.lisp *
- books/meta/Makefile *
- books/meta/README *
- books/meta/certify.lsp *
- books/meta/meta-plus-equal.lisp *
- books/meta/meta-plus-lessp.lisp *
- books/meta/meta-times-equal.lisp *
- books/meta/meta.lisp *
- books/meta/pseudo-termp-lemmas.lisp *
- books/meta/term-defuns.lisp *
- books/meta/term-lemmas.lisp *
- books/misc/certify.lsp *
- books/misc/computed-hint.lisp *
- books/misc/csort.lisp *
- books/misc/dft-ex.acl2 *
- books/misc/dft-ex.lisp *
- books/misc/dft.lisp *
- books/misc/dump-events.lisp *
- books/misc/fibonacci.lisp *
- books/misc/grcd.lisp *
- books/misc/int-division.lisp *
- books/misc/meta-lemmas.lisp *
- books/misc/mult.lisp *
- books/misc/priorities.lisp *
- books/misc/problem13.lisp *
- books/misc/records.lisp *
- books/misc/records0.lisp *
- books/misc/sin-cos.lisp *
- books/misc/symbol-btree.lisp *
- books/misc/total-order.lisp *
- books/ordinals/Makefile *
- books/ordinals/certify.lsp *
- books/ordinals/limits.lisp *
- books/ordinals/ordinal-addition.lisp *
- books/ordinals/ordinal-basic-thms.lisp *
- books/ordinals/ordinal-counter-examples.lisp *
- books/ordinals/ordinal-definitions.lisp *
- books/ordinals/ordinal-isomorphism.lisp *
- books/ordinals/ordinal-multiplication.lisp *
- books/ordinals/ordinal-total-order.lisp *
- books/ordinals/ordinals-without-arithmetic.lisp *
- books/ordinals/ordinals.lisp *
- books/ordinals/top-with-meta.lisp *
- books/powerlists/Makefile *
- books/powerlists/README *
- books/powerlists/algebra.acl2 *
- books/powerlists/algebra.lisp *
- books/powerlists/batcher-sort.acl2 *
- books/powerlists/batcher-sort.lisp *
- books/powerlists/bitonic-sort.acl2 *
- books/powerlists/bitonic-sort.lisp *
- books/powerlists/certify.lsp *
- books/powerlists/cla-adder.acl2 *
- books/powerlists/cla-adder.lisp *
- books/powerlists/defpkg.lisp *
- books/powerlists/gray-code.acl2 *
- books/powerlists/gray-code.lisp *
- books/powerlists/merge-sort.acl2 *
- books/powerlists/merge-sort.lisp *
- books/powerlists/prefix-sum.acl2 *
- books/powerlists/prefix-sum.lisp *
- books/powerlists/simple.acl2 *
- books/powerlists/simple.lisp *
- books/powerlists/sort.acl2 *
- books/powerlists/sort.lisp *
- books/rtl/rel1/Makefile *
- books/rtl/rel1/README *
- books/rtl/rel1/lib1/Makefile *
- books/rtl/rel1/lib1/basic.lisp *
- books/rtl/rel1/lib1/bits.lisp *
- books/rtl/rel1/lib1/brat.lisp *
- books/rtl/rel1/lib1/reps.lisp *
- books/rtl/rel1/lib1/top.lisp *
- books/rtl/rel1/lib3/Makefile *
- books/rtl/rel1/lib3/basic.lisp *
- books/rtl/rel1/lib3/bits.lisp *
- books/rtl/rel1/lib3/brat.lisp *
- books/rtl/rel1/lib3/fadd.lisp *
- books/rtl/rel1/lib3/reps.lisp *
- books/rtl/rel1/lib3/top.lisp *
- books/rtl/rel1/support/Makefile *
- books/rtl/rel1/support/add.lisp *
- books/rtl/rel1/support/away.lisp *
- books/rtl/rel1/support/basic.lisp *
- books/rtl/rel1/support/divsqrt.lisp *
- books/rtl/rel1/support/fadd/Makefile *
- books/rtl/rel1/support/fadd/add3.lisp *
- books/rtl/rel1/support/fadd/lop1.lisp *
- books/rtl/rel1/support/fadd/lop2.lisp *
- books/rtl/rel1/support/fadd/lop3.lisp *
- books/rtl/rel1/support/fadd/stick.lisp *
- books/rtl/rel1/support/fadd/top.lisp *
- books/rtl/rel1/support/float.lisp *
- books/rtl/rel1/support/floor.lisp *
- books/rtl/rel1/support/fp.lisp *
- books/rtl/rel1/support/logdefs.lisp *
- books/rtl/rel1/support/loglemmas.lisp *
- books/rtl/rel1/support/logxor-def.lisp *
- books/rtl/rel1/support/logxor-lemmas.lisp *
- books/rtl/rel1/support/near.lisp *
- books/rtl/rel1/support/odd.lisp *
- books/rtl/rel1/support/proofs.lisp *
- books/rtl/rel1/support/reps.lisp *
- books/rtl/rel1/support/rewrite-theory.lisp *
- books/rtl/rel1/support/rnd.lisp *
- books/rtl/rel1/support/sticky.lisp *
- books/rtl/rel1/support/trunc.lisp *
- books/rtl/rel1/support/x-2xx.lisp *
- doc/HTML/llogo.gif *
- doc/HTML/logo.gif *
- doc/create-acl2-html *
added
removed
proof-checker-pkg.lisp
