[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general updated (20412f1 -> 1b1083e)
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general updated (20412f1 -> 1b1083e) |
|
Date: |
Thu, 25 Nov 2021 10:57:56 -0500 (EST) |
elpasync pushed a change to branch elpa/proof-general.
from 20412f1 Merge pull request #629 from
Matafou/fix-#625-indentation-is-slow
new 1931c8c Remove Twelf support
new 48bd86b Remove HOL98 support
new 73571a5 Remove CCC support
new 8b16d1d Remove LEGO support
new 23f7895 Remove Hol-Light support
new da5f073 Remove ACL2 support
new 0a295cd Remove Plastic support
new e27b1ef Remove Lambda-Clam support
new 511226f Remove Isabelle/Isar support
new 497709f AUTHORS: Add notes about copyright status
new f99cdf2 Misc cosmetic tweaks that occurred during GPLv3+ license
work
new 6c9c995 Change the license to GPLv3+ (Fix #198)
new 1b1083e Merge pull request #627 from ProofGeneral/scratch-GPLv3
Summary of changes:
AUTHORS | 30 +
BUGS | 22 +-
CHANGES | 3 +
COPYING | 912 ++++---
INSTALL | 6 +-
Makefile | 48 +-
Makefile.devel | 2 +-
README.md | 19 +-
acl2/README | 22 -
acl2/acl2.el | 106 -
acl2/example.acl2 | 9 -
acl2/root2.acl2 | 348 ---
ccc/README | 14 -
ccc/ccc.el | 85 -
ci/compile-tests/001-mini-project/Makefile | 2 +-
ci/compile-tests/001-mini-project/a.v | 2 +-
ci/compile-tests/001-mini-project/b.v | 2 +-
ci/compile-tests/001-mini-project/c.v | 2 +-
ci/compile-tests/001-mini-project/d.v | 2 +-
ci/compile-tests/001-mini-project/e.v | 2 +-
ci/compile-tests/001-mini-project/f.v | 2 +-
ci/compile-tests/001-mini-project/runtest.el | 2 +-
.../002-require-no-dependencies/Makefile | 2 +-
ci/compile-tests/002-require-no-dependencies/a.v | 2 +-
ci/compile-tests/002-require-no-dependencies/b.v | 2 +-
ci/compile-tests/002-require-no-dependencies/c.v | 2 +-
.../002-require-no-dependencies/runtest.el | 2 +-
ci/compile-tests/003-require-error/Makefile | 2 +-
ci/compile-tests/003-require-error/a.v | 2 +-
ci/compile-tests/003-require-error/b.v | 2 +-
ci/compile-tests/003-require-error/c.v | 2 +-
ci/compile-tests/003-require-error/runtest.el | 2 +-
ci/compile-tests/004-dependency-cycle/Makefile | 2 +-
ci/compile-tests/004-dependency-cycle/a.v | 2 +-
ci/compile-tests/004-dependency-cycle/b.v | 2 +-
ci/compile-tests/004-dependency-cycle/c.v | 2 +-
ci/compile-tests/004-dependency-cycle/d.v | 2 +-
ci/compile-tests/004-dependency-cycle/e.v | 2 +-
ci/compile-tests/004-dependency-cycle/f.v | 2 +-
ci/compile-tests/004-dependency-cycle/runtest.el | 2 +-
ci/compile-tests/005-change-recompile/Makefile | 2 +-
ci/compile-tests/005-change-recompile/a.v.orig | 2 +-
ci/compile-tests/005-change-recompile/b.v.orig | 2 +-
ci/compile-tests/005-change-recompile/c.v.orig | 2 +-
ci/compile-tests/005-change-recompile/d.v.orig | 2 +-
ci/compile-tests/005-change-recompile/e.v.orig | 2 +-
ci/compile-tests/005-change-recompile/f.v.orig | 2 +-
ci/compile-tests/005-change-recompile/g.v.orig | 2 +-
ci/compile-tests/005-change-recompile/h.v.orig | 2 +-
ci/compile-tests/005-change-recompile/runtest.el | 2 +-
ci/compile-tests/006-ready-dependee/Makefile | 2 +-
ci/compile-tests/006-ready-dependee/a.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/b.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/c.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/d.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/e.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/f.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/g.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/h.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/i.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/j.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/k.v.orig | 2 +-
ci/compile-tests/006-ready-dependee/runtest.el | 2 +-
ci/compile-tests/007-slow-require/Makefile | 2 +-
ci/compile-tests/007-slow-require/a1.v.orig | 2 +-
ci/compile-tests/007-slow-require/a2.v.orig | 2 +-
ci/compile-tests/007-slow-require/a3.v.orig | 2 +-
ci/compile-tests/007-slow-require/a4.v.orig | 2 +-
ci/compile-tests/007-slow-require/a5.v.orig | 2 +-
ci/compile-tests/007-slow-require/a6.v.orig | 2 +-
ci/compile-tests/007-slow-require/b1.v.orig | 2 +-
ci/compile-tests/007-slow-require/b2.v.orig | 2 +-
ci/compile-tests/007-slow-require/b3.v.orig | 2 +-
ci/compile-tests/007-slow-require/b4.v.orig | 2 +-
ci/compile-tests/007-slow-require/b5.v.orig | 2 +-
ci/compile-tests/007-slow-require/b6.v.orig | 2 +-
ci/compile-tests/007-slow-require/c1.v.orig | 2 +-
ci/compile-tests/007-slow-require/c2.v.orig | 2 +-
ci/compile-tests/007-slow-require/c3.v.orig | 2 +-
ci/compile-tests/007-slow-require/c4.v.orig | 2 +-
ci/compile-tests/007-slow-require/c5.v.orig | 2 +-
ci/compile-tests/007-slow-require/c6.v.orig | 2 +-
ci/compile-tests/007-slow-require/d1.v.orig | 2 +-
ci/compile-tests/007-slow-require/d2.v.orig | 2 +-
ci/compile-tests/007-slow-require/d3.v.orig | 2 +-
ci/compile-tests/007-slow-require/d4.v.orig | 2 +-
ci/compile-tests/007-slow-require/d5.v.orig | 2 +-
ci/compile-tests/007-slow-require/d6.v.orig | 2 +-
ci/compile-tests/007-slow-require/runtest.el | 2 +-
ci/compile-tests/008-default-dir/Makefile | 2 +-
ci/compile-tests/008-default-dir/a.v.orig | 2 +-
ci/compile-tests/008-default-dir/b.v.orig | 2 +-
ci/compile-tests/008-default-dir/c.v.orig | 2 +-
ci/compile-tests/008-default-dir/runtest.el | 2 +-
ci/compile-tests/009-failure-processing/Makefile | 2 +-
ci/compile-tests/009-failure-processing/a1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/a9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/b9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/c9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/d9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/e9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/f9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/g9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h1.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h10.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h2.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h3.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h4.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h5.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h6.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h7.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h8.v.orig | 2 +-
ci/compile-tests/009-failure-processing/h9.v.orig | 2 +-
ci/compile-tests/009-failure-processing/runtest.el | 2 +-
ci/compile-tests/Makefile | 2 +-
ci/compile-tests/bin/compile-test-start-delayed | 2 +-
ci/compile-tests/cct-lib.el | 2 +-
ci/simple-tests/Makefile | 2 +-
.../test-coq-par-job-needs-compilation-quick.el | 2 +-
ci/simple-tests/test-coqtop-unavailable.el | 2 +-
ci/simple-tests/test-omit-proofs.el | 2 +-
ci/simple-tests/test-prelude-correct.el | 2 +-
ci/test-indent/Makefile | 2 +-
coq/coq-abbrev.el | 2 +-
coq/coq-compile-common.el | 2 +-
coq/coq-db.el | 2 +-
coq/coq-diffs.el | 2 +-
coq/coq-mode.el | 2 +-
coq/coq-par-compile.el | 2 +-
coq/coq-seq-compile.el | 2 +-
coq/coq-smie.el | 2 +-
coq/coq-syntax.el | 2 +-
coq/coq-system.el | 2 +-
coq/coq.el | 2 +-
doc/PG-adapting.texi | 26 +-
doc/ProofGeneral.texi | 527 +---
doc/proofgeneral.1 | 4 +-
etc/ProofGeneral.spec | 4 +-
etc/README | 3 -
etc/hol-light/example4.ml | 13 -
etc/isar/AHundredProofs.thy | 1009 --------
etc/isar/AHundredTheorems.thy | 117 -
etc/isar/AThousandComments.thy | 1005 --------
etc/isar/AThousandTheorems.thy | 1013 --------
etc/isar/BackslashInStrings.thy | 47 -
etc/isar/BigErrors.thy | 20 -
etc/isar/BigErrorsNested.thy | 6 -
etc/isar/ChosenLogic.thy | 8 -
etc/isar/ChosenLogic2.thy | 8 -
etc/isar/CommentParsingBug.thy | 3 -
etc/isar/CommentParsingBug2.thy | 8 -
etc/isar/Depends.thy | 14 -
etc/isar/EmptyCommands.thy | 10 -
etc/isar/FaultyErrors.thy | 28 -
etc/isar/Fibonacci.thy | 168 --
etc/isar/HighlightSize.thy | 13 -
etc/isar/IllegalEscape.thy | 7 -
etc/isar/InterruptTest.thy.gz | Bin 3914 -> 0 bytes
etc/isar/MultipleModes.thy | 27 -
etc/isar/NamesInStrings.thy | 34 -
etc/isar/Parsing.thy | 75 -
etc/isar/ParsingBug1.thy | 15 -
etc/isar/Persistent.thy | 40 -
etc/isar/README | 8 -
etc/isar/Sendback.thy | 23 -
etc/isar/TextProps.thy | 22 -
etc/isar/TokensAcid.thy | 218 --
etc/isar/Trac189.thy | 8 -
etc/isar/Trac280-subrev.thy | 14 -
etc/isar/Unicode.thy | 73 -
etc/isar/XEmacsSyntacticContextProb.thy | 20 -
etc/isar/XSymbolTests.thy | 146 --
etc/isar/bad1.thy | 3 -
etc/isar/bad2.thy | 1 -
etc/isar/multiple/A.thy | 7 -
etc/isar/multiple/B.thy | 4 -
etc/isar/multiple/C.thy | 4 -
etc/isar/multiple/D.thy | 4 -
etc/isar/multiple/E.thy | 4 -
etc/isar/multiple/README | 3 -
etc/isar/nesting-too-deep-for-parser.txt | 1622 ------------
etc/isar/new-parsing-test.el | 38 -
etc/isar/profiling.txt | 322 ---
etc/isar/trace_simp.thy | 20 -
etc/lego/GoalGoal.l | 13 -
etc/lego/error-eg.l | 16 -
etc/lego/lego-site.el | 37 -
etc/lego/long-line-backslash.l | 22 -
etc/lego/multiple/A.l | 1 -
etc/lego/multiple/B.l | 4 -
etc/lego/multiple/C.l | 1 -
etc/lego/multiple/D.l | 1 -
etc/lego/multiple/README | 33 -
etc/lego/pbp.l | 30 -
etc/lego/unsaved-goals.l | 54 -
generic/pg-assoc.el | 2 +-
generic/pg-autotest.el | 2 +-
generic/pg-custom.el | 12 +-
generic/pg-goals.el | 2 +-
generic/pg-movie.el | 2 +-
generic/pg-pbrpm.el | 2 +-
generic/pg-pgip.el | 2 +-
generic/pg-response.el | 6 +-
generic/pg-user.el | 2 +-
generic/pg-vars.el | 2 +-
generic/pg-xml.el | 2 +-
generic/proof-auxmodes.el | 2 +-
generic/proof-config.el | 37 +-
generic/proof-depends.el | 4 +-
generic/proof-easy-config.el | 2 +-
generic/proof-faces.el | 2 +-
generic/proof-indent.el | 2 +-
generic/proof-maths-menu.el | 2 +-
generic/proof-menu.el | 2 +-
generic/proof-script.el | 13 +-
generic/proof-shell.el | 8 +-
generic/proof-site.el | 17 +-
generic/proof-splash.el | 2 +-
generic/proof-syntax.el | 2 +-
generic/proof-toolbar.el | 2 +-
generic/proof-tree.el | 2 +-
generic/proof-unicode-tokens.el | 2 +-
generic/proof-useropts.el | 8 +-
generic/proof-utils.el | 2 +-
generic/proof.el | 2 +-
hol-light/LICENSE-HOL-LIGHT | 29 -
hol-light/README | 45 -
hol-light/TODO | 17 -
hol-light/TacticRecording/INSTRUCTIONS | 36 -
hol-light/TacticRecording/LIMITATIONS | 18 -
hol-light/TacticRecording/biolayout.ml | 30 -
hol-light/TacticRecording/dltree.ml | 268 --
hol-light/TacticRecording/dltree.mli | 22 -
hol-light/TacticRecording/ex.dot | 24 -
hol-light/TacticRecording/ex2.dot | 13 -
hol-light/TacticRecording/ex3.dot | 24 -
hol-light/TacticRecording/ex3.png | Bin 39644 -> 0 bytes
hol-light/TacticRecording/ex3b.dot | 37 -
hol-light/TacticRecording/examples1.ml | 64 -
hol-light/TacticRecording/examples1_output.txt | 72 -
hol-light/TacticRecording/examples2.ml | 45 -
hol-light/TacticRecording/examples3.ml | 236 --
hol-light/TacticRecording/examples3_LEMMA1.dot | 24 -
hol-light/TacticRecording/examples3_output.txt | 36 -
hol-light/TacticRecording/examples4.ml | 13 -
hol-light/TacticRecording/examples5.ml | 182 --
hol-light/TacticRecording/gvexport.ml | 47 -
hol-light/TacticRecording/hiproofs.ml | 417 ---
hol-light/TacticRecording/lib.ml | 91 -
hol-light/TacticRecording/main.ml | 31 -
hol-light/TacticRecording/mldata.ml | 33 -
hol-light/TacticRecording/mlexport.ml | 186 --
hol-light/TacticRecording/printutils.ml | 61 -
hol-light/TacticRecording/promote.ml | 327 ---
hol-light/TacticRecording/prooftree.ml | 177 --
hol-light/TacticRecording/tacticrec.ml | 383 ---
hol-light/TacticRecording/wrappers.ml | 359 ---
hol-light/TacticRecording/xtactics.ml | 451 ----
hol-light/TacticRecording/xthm.ml | 40 -
hol-light/example.ml | 19 -
hol-light/hol-light-autotest.el | 42 -
hol-light/hol-light-unicode-tokens.el | 252 --
hol-light/hol-light.el | 519 ----
hol-light/pg_prompt.ml | 59 -
hol-light/pg_tactics.ml | 349 ---
hol-light/temp-prooftree-configure.patch | 25 -
hol98/README | 53 -
hol98/example.sml | 30 -
hol98/hol98.el | 170 --
hol98/root2.sml | 83 -
isar/Example-Tokens.thy | 37 -
isar/Example.thy | 33 -
isar/README | 33 -
isar/ex/Knaster_Tarski.thy | 110 -
isar/ex/PER.thy | 269 --
isar/ex/README | 8 -
isar/ex/Sqrt.thy | 90 -
isar/ex/Sqrt_Script.thy | 70 -
isar/ex/Tarski.thy | 927 -------
isar/interface | 205 --
isar/interface-setup.el | 40 -
isar/isabelle-system.el | 375 ---
isar/isar-autotest.el | 117 -
isar/isar-find-theorems.el | 489 ----
isar/isar-keywords.el | 655 -----
isar/isar-profiling.el | 58 -
isar/isar-syntax.el | 612 -----
isar/isar-unicode-tokens.el | 691 -----
isar/isar.el | 645 -----
isar/isartags | 86 -
lego/BUGS | 53 -
lego/README | 37 -
lego/example.l | 15 -
lego/example2.l | 1 -
lego/lego-syntax.el | 131 -
lego/lego.el | 439 ----
lego/legotags | 91 -
lego/root2.l | 368 ---
lib/bufhist.el | 4 +-
lib/holes.el | 6 +-
lib/local-vars-list.el | 16 +-
lib/maths-menu.el | 2 +-
lib/pg-dev.el | 10 +-
lib/pg-fontsets.el | 2 +-
lib/proof-compat.el | 2 +-
lib/scomint.el | 2 +-
lib/span.el | 2 +-
lib/texi-docstring-magic.el | 4 +-
lib/unicode-tokens.el | 4 +-
obsolete/demoisa/demoisa.el | 2 +-
obsolete/lclam/README | 15 -
obsolete/lclam/example.lcm | 34 -
obsolete/lclam/lclam.el | 209 --
obsolete/plastic/README | 12 -
obsolete/plastic/plastic-syntax.el | 119 -
obsolete/plastic/plastic.el | 665 -----
obsolete/plastic/test.lf | 64 -
proof-general.el | 19 +-
twelf/README | 27 -
twelf/example.elf | 64 -
twelf/twelf-font.el | 444 ----
twelf/twelf-old.el | 2660 --------------------
twelf/twelf.el | 209 --
385 files changed, 1029 insertions(+), 24859 deletions(-)
delete mode 100644 acl2/README
delete mode 100644 acl2/acl2.el
delete mode 100644 acl2/example.acl2
delete mode 100644 acl2/root2.acl2
delete mode 100644 ccc/README
delete mode 100644 ccc/ccc.el
delete mode 100644 etc/hol-light/example4.ml
delete mode 100644 etc/isar/AHundredProofs.thy
delete mode 100644 etc/isar/AHundredTheorems.thy
delete mode 100644 etc/isar/AThousandComments.thy
delete mode 100644 etc/isar/AThousandTheorems.thy
delete mode 100644 etc/isar/BackslashInStrings.thy
delete mode 100644 etc/isar/BigErrors.thy
delete mode 100644 etc/isar/BigErrorsNested.thy
delete mode 100644 etc/isar/ChosenLogic.thy
delete mode 100644 etc/isar/ChosenLogic2.thy
delete mode 100644 etc/isar/CommentParsingBug.thy
delete mode 100644 etc/isar/CommentParsingBug2.thy
delete mode 100644 etc/isar/Depends.thy
delete mode 100644 etc/isar/EmptyCommands.thy
delete mode 100644 etc/isar/FaultyErrors.thy
delete mode 100644 etc/isar/Fibonacci.thy
delete mode 100644 etc/isar/HighlightSize.thy
delete mode 100644 etc/isar/IllegalEscape.thy
delete mode 100644 etc/isar/InterruptTest.thy.gz
delete mode 100644 etc/isar/MultipleModes.thy
delete mode 100644 etc/isar/NamesInStrings.thy
delete mode 100644 etc/isar/Parsing.thy
delete mode 100644 etc/isar/ParsingBug1.thy
delete mode 100644 etc/isar/Persistent.thy
delete mode 100644 etc/isar/README
delete mode 100644 etc/isar/Sendback.thy
delete mode 100644 etc/isar/TextProps.thy
delete mode 100644 etc/isar/TokensAcid.thy
delete mode 100644 etc/isar/Trac189.thy
delete mode 100644 etc/isar/Trac280-subrev.thy
delete mode 100644 etc/isar/Unicode.thy
delete mode 100644 etc/isar/XEmacsSyntacticContextProb.thy
delete mode 100644 etc/isar/XSymbolTests.thy
delete mode 100644 etc/isar/bad1.thy
delete mode 100644 etc/isar/bad2.thy
delete mode 100644 etc/isar/multiple/A.thy
delete mode 100644 etc/isar/multiple/B.thy
delete mode 100644 etc/isar/multiple/C.thy
delete mode 100644 etc/isar/multiple/D.thy
delete mode 100644 etc/isar/multiple/E.thy
delete mode 100644 etc/isar/multiple/README
delete mode 100644 etc/isar/nesting-too-deep-for-parser.txt
delete mode 100644 etc/isar/new-parsing-test.el
delete mode 100644 etc/isar/profiling.txt
delete mode 100644 etc/isar/trace_simp.thy
delete mode 100644 etc/lego/GoalGoal.l
delete mode 100644 etc/lego/error-eg.l
delete mode 100644 etc/lego/lego-site.el
delete mode 100644 etc/lego/long-line-backslash.l
delete mode 100644 etc/lego/multiple/A.l
delete mode 100644 etc/lego/multiple/B.l
delete mode 100644 etc/lego/multiple/C.l
delete mode 100644 etc/lego/multiple/D.l
delete mode 100644 etc/lego/multiple/README
delete mode 100644 etc/lego/pbp.l
delete mode 100644 etc/lego/unsaved-goals.l
delete mode 100644 hol-light/LICENSE-HOL-LIGHT
delete mode 100644 hol-light/README
delete mode 100644 hol-light/TODO
delete mode 100644 hol-light/TacticRecording/INSTRUCTIONS
delete mode 100644 hol-light/TacticRecording/LIMITATIONS
delete mode 100644 hol-light/TacticRecording/biolayout.ml
delete mode 100644 hol-light/TacticRecording/dltree.ml
delete mode 100644 hol-light/TacticRecording/dltree.mli
delete mode 100644 hol-light/TacticRecording/ex.dot
delete mode 100644 hol-light/TacticRecording/ex2.dot
delete mode 100644 hol-light/TacticRecording/ex3.dot
delete mode 100644 hol-light/TacticRecording/ex3.png
delete mode 100644 hol-light/TacticRecording/ex3b.dot
delete mode 100644 hol-light/TacticRecording/examples1.ml
delete mode 100644 hol-light/TacticRecording/examples1_output.txt
delete mode 100644 hol-light/TacticRecording/examples2.ml
delete mode 100644 hol-light/TacticRecording/examples3.ml
delete mode 100644 hol-light/TacticRecording/examples3_LEMMA1.dot
delete mode 100644 hol-light/TacticRecording/examples3_output.txt
delete mode 100644 hol-light/TacticRecording/examples4.ml
delete mode 100644 hol-light/TacticRecording/examples5.ml
delete mode 100644 hol-light/TacticRecording/gvexport.ml
delete mode 100644 hol-light/TacticRecording/hiproofs.ml
delete mode 100644 hol-light/TacticRecording/lib.ml
delete mode 100644 hol-light/TacticRecording/main.ml
delete mode 100644 hol-light/TacticRecording/mldata.ml
delete mode 100644 hol-light/TacticRecording/mlexport.ml
delete mode 100644 hol-light/TacticRecording/printutils.ml
delete mode 100644 hol-light/TacticRecording/promote.ml
delete mode 100644 hol-light/TacticRecording/prooftree.ml
delete mode 100644 hol-light/TacticRecording/tacticrec.ml
delete mode 100644 hol-light/TacticRecording/wrappers.ml
delete mode 100644 hol-light/TacticRecording/xtactics.ml
delete mode 100644 hol-light/TacticRecording/xthm.ml
delete mode 100644 hol-light/example.ml
delete mode 100644 hol-light/hol-light-autotest.el
delete mode 100644 hol-light/hol-light-unicode-tokens.el
delete mode 100644 hol-light/hol-light.el
delete mode 100644 hol-light/pg_prompt.ml
delete mode 100644 hol-light/pg_tactics.ml
delete mode 100644 hol-light/temp-prooftree-configure.patch
delete mode 100644 hol98/README
delete mode 100644 hol98/example.sml
delete mode 100644 hol98/hol98.el
delete mode 100644 hol98/root2.sml
delete mode 100644 isar/Example-Tokens.thy
delete mode 100644 isar/Example.thy
delete mode 100644 isar/README
delete mode 100644 isar/ex/Knaster_Tarski.thy
delete mode 100644 isar/ex/PER.thy
delete mode 100644 isar/ex/README
delete mode 100644 isar/ex/Sqrt.thy
delete mode 100644 isar/ex/Sqrt_Script.thy
delete mode 100644 isar/ex/Tarski.thy
delete mode 100755 isar/interface
delete mode 100644 isar/interface-setup.el
delete mode 100644 isar/isabelle-system.el
delete mode 100644 isar/isar-autotest.el
delete mode 100644 isar/isar-find-theorems.el
delete mode 100644 isar/isar-keywords.el
delete mode 100644 isar/isar-profiling.el
delete mode 100644 isar/isar-syntax.el
delete mode 100644 isar/isar-unicode-tokens.el
delete mode 100644 isar/isar.el
delete mode 100755 isar/isartags
delete mode 100644 lego/BUGS
delete mode 100644 lego/README
delete mode 100644 lego/example.l
delete mode 100644 lego/example2.l
delete mode 100644 lego/lego-syntax.el
delete mode 100644 lego/lego.el
delete mode 100755 lego/legotags
delete mode 100644 lego/root2.l
delete mode 100644 obsolete/lclam/README
delete mode 100644 obsolete/lclam/example.lcm
delete mode 100644 obsolete/lclam/lclam.el
delete mode 100644 obsolete/plastic/README
delete mode 100644 obsolete/plastic/plastic-syntax.el
delete mode 100644 obsolete/plastic/plastic.el
delete mode 100644 obsolete/plastic/test.lf
delete mode 100644 twelf/README
delete mode 100644 twelf/example.elf
delete mode 100644 twelf/twelf-font.el
delete mode 100644 twelf/twelf-old.el
delete mode 100644 twelf/twelf.el
- [nongnu] elpa/proof-general updated (20412f1 -> 1b1083e),
ELPA Syncer <=
- [nongnu] elpa/proof-general 1931c8c 01/13: Remove Twelf support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 48bd86b 02/13: Remove HOL98 support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 73571a5 03/13: Remove CCC support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 8b16d1d 04/13: Remove LEGO support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 23f7895 05/13: Remove Hol-Light support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 6c9c995 12/13: Change the license to GPLv3+ (Fix #198), ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 511226f 09/13: Remove Isabelle/Isar support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 497709f 10/13: AUTHORS: Add notes about copyright status, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 0a295cd 07/13: Remove Plastic support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general e27b1ef 08/13: Remove Lambda-Clam support, ELPA Syncer, 2021/11/25