| #
fed9d1bd |
|
25-Oct-2019 |
blanchet <none@none> |
added support for Zipperposition on SystemOnTPTP
|
| #
c16c77d9 |
|
25-Oct-2019 |
blanchet <none@none> |
removed support for old system E-MaLeS
|
| #
a9bcfce5 |
|
25-Oct-2019 |
blanchet <none@none> |
added support for repote Alt-Ergo
|
| #
fb7ae96d |
|
25-Oct-2019 |
blanchet <none@none> |
updated nomenclature for TPTP languages to use modern three-symbol abbreviations (e.g. TF1)
|
| #
24bc4833 |
|
25-Oct-2019 |
blanchet <none@none> |
removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0
|
| #
b97e6dae |
|
25-Oct-2019 |
blanchet <none@none> |
removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
|
| #
e9fea14f |
|
25-Oct-2019 |
blanchet <none@none> |
removed support for iProver-Eq
|
| #
38e42120 |
|
25-Oct-2019 |
blanchet <none@none> |
updated iProver setup and tuned other ATP setups
|
| #
d7101e4b |
|
25-Oct-2019 |
blanchet <none@none> |
removed support for remote Satallax because its output does not clearly identify the lemmas used
|
| #
9021a9f0 |
|
25-Oct-2019 |
blanchet <none@none> |
changed Satallax's setup to invoke E
|
| #
d7037b5f |
|
10-Oct-2019 |
blanchet <none@none> |
updated veriT part of Sledgehammer documentation
|
| #
a3f9e217 |
|
10-Oct-2019 |
blanchet <none@none> |
added para constrasting 'primrec' and 'fun' -- and removed my middle name
|
| #
7c718ad5 |
|
18-Jul-2018 |
wenzelm <none@none> |
prefer HTTPS;
|
| #
b3fa57f8 |
|
02-Jul-2018 |
blanchet <none@none> |
update Sledgehammer docs w.r.t. Vampire
|
| #
2a2b07a9 |
|
22-May-2018 |
blanchet <none@none> |
added lambda-free HO output for Ehoh (higher-order E prototype)
|
| #
43189320 |
|
07-Nov-2017 |
blanchet <none@none> |
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
|
| #
8c3c79d4 |
|
30-Sep-2017 |
blanchet <none@none> |
updated Sledgehammer docs
|
| #
636bdd0e |
|
07-Aug-2017 |
blanchet <none@none> |
use TFF0 with E 2.0 and above
|
| #
796b0ae2 |
|
20-Apr-2017 |
blanchet <none@none> |
removed French accent from docs
|
| #
d77b938a |
|
30-Aug-2016 |
blanchet <none@none> |
tuned docs
|
| #
1894861c |
|
27-Mar-2016 |
blanchet <none@none> |
updated Sledgehammer documentation
|
| #
d50d27cf |
|
02-Oct-2015 |
blanchet <none@none> |
updated docs and NEWS
|
| #
c330ca9a |
|
02-Oct-2015 |
blanchet <none@none> |
removed obsolete material in documentation
|
| #
52f8f6cb |
|
30-Sep-2015 |
blanchet <none@none> |
updated docs
|
| #
d0b8a95b |
|
28-Aug-2015 |
blanchet <none@none> |
eliminated obsolete environment variable
|
| #
a5e636ff |
|
24-Jun-2015 |
blanchet <none@none> |
put E before (typically remote, hence less reliable) Vampire
|
| #
d475a1c7 |
|
28-May-2015 |
blanchet <none@none> |
made Auto Sledgehammer behave more like the real thing
|
| #
50e6a752 |
|
23-May-2015 |
wenzelm <none@none> |
prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
|
| #
73630cc3 |
|
08-Apr-2015 |
blanchet <none@none> |
updated docs to reflect actually run ATPs
|
| #
13fed95d |
|
08-Apr-2015 |
blanchet <none@none> |
updated docs to Z3 open source
|
| #
5091b5ae |
|
03-Mar-2015 |
blanchet <none@none> |
SPASS-Pirate is now called Pirate
--HG--
rename : src/HOL/Tools/ATP/scripts/remote_spass_pirate => src/HOL/Tools/ATP/scripts/remote_pirate
|
| #
5cece74c |
|
11-Feb-2015 |
blanchet <none@none> |
updated Sledgehammer docs
|
| #
28085c4a |
|
23-Nov-2014 |
blanchet <none@none> |
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
|
| #
e7563ab1 |
|
23-Nov-2014 |
blanchet <none@none> |
update CVC4 version docs
|
| #
36261023 |
|
30-Sep-2014 |
blanchet <none@none> |
updated docs with two provers: veriT and Zipperposition
|
| #
e927f863 |
|
28-Aug-2014 |
blanchet <none@none> |
clarified docs
|
| #
915c1c6b |
|
04-Aug-2014 |
blanchet <none@none> |
updated 'compress' docs
|
| #
6c7ff185 |
|
24-Jul-2014 |
blanchet <none@none> |
reenabled MaSh for Isabelle2014 release (hopefully)
|
| #
c791c7ee |
|
23-Jul-2014 |
blanchet <none@none> |
stick to external proofs when invoking E, because they are more detailed and do not merge steps
|
| #
4a341ec2 |
|
16-Jul-2014 |
blanchet <none@none> |
disabled MaSh for the Isabelle2014 release, due to a couple of issues
|
| #
44cfbb1a |
|
09-Jul-2014 |
blanchet <none@none> |
improved docs
|
| #
96f18c51 |
|
09-Jul-2014 |
blanchet <none@none> |
tuned terminology
|
| #
9faf162f |
|
01-Jul-2014 |
blanchet <none@none> |
updated docs
|
| #
3842fa63 |
|
29-Jun-2014 |
blanchet <none@none> |
killed Python version of MaSh, now that the SML version works adequately
|
| #
370826ee |
|
01-Aug-2014 |
blanchet <none@none> |
update documentation after removal of 'min' subcommand
|
| #
ea5faa03 |
|
01-Aug-2014 |
blanchet <none@none> |
removed proof methods as provers from docs
|
| #
c427256a |
|
30-Jul-2014 |
blanchet <none@none> |
updated docs
|
| #
a7c21884 |
|
30-Jul-2014 |
blanchet <none@none> |
reduced preplay timeout to 1 s
|
| #
b1b56291 |
|
18-Jun-2014 |
blanchet <none@none> |
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
|
| #
047b3f9c |
|
12-Jun-2014 |
blanchet <none@none> |
renamed Sledgehammer options
|
| #
4262089d |
|
12-Jun-2014 |
blanchet <none@none> |
updated docs
|
| #
5367ddba |
|
12-Jun-2014 |
blanchet <none@none> |
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
|
| #
16f7ff50 |
|
11-Jun-2014 |
blanchet <none@none> |
updated docs w.r.t. Z3
|
| #
6b6b8c04 |
|
28-May-2014 |
blanchet <none@none> |
changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
|
| #
60b7611a |
|
27-May-2014 |
blanchet <none@none> |
updated naive Bayes
|
| #
feafc9a8 |
|
26-May-2014 |
blanchet <none@none> |
renamed 'MaSh' option
|
| #
59db6ad2 |
|
21-May-2014 |
blanchet <none@none> |
shorten Sledgehammer output, as suggested by Andrei Popescu
|
| #
3f109b55 |
|
21-May-2014 |
blanchet <none@none> |
docs
|
| #
e18d3525 |
|
20-May-2014 |
blanchet <none@none> |
added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
|
| #
15551912 |
|
20-May-2014 |
blanchet <none@none> |
added Isabelle system option 'mash'
|
| #
0d6c971d |
|
20-May-2014 |
blanchet <none@none> |
updated docs
|
| #
374ac6a3 |
|
25-Apr-2014 |
blanchet <none@none> |
updated Z3 version number
|
| #
f046f465 |
|
03-Apr-2014 |
blanchet <none@none> |
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
|
| #
919c980b |
|
03-Apr-2014 |
blanchet <none@none> |
use Alt-Ergo 0.95.2, the latest and greatest version
|
| #
77d94ba9 |
|
03-Apr-2014 |
blanchet <none@none> |
updated Z3 TPTP to 4.3.1+
|
| #
be333129 |
|
03-Apr-2014 |
blanchet <none@none> |
updated Why3 version in docs
|
| #
4f9e00aa |
|
13-Mar-2014 |
blanchet <none@none> |
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
|
| #
fc221c95 |
|
13-Mar-2014 |
blanchet <none@none> |
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
|
| #
7bdabf18 |
|
05-Feb-2014 |
blanchet <none@none> |
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
|
| #
9a5b75f2 |
|
03-Feb-2014 |
blanchet <none@none> |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
| #
e66f9d0c |
|
03-Feb-2014 |
blanchet <none@none> |
reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
|
| #
47168367 |
|
03-Feb-2014 |
blanchet <none@none> |
searchable underscores
|
| #
5c32047b |
|
03-Feb-2014 |
blanchet <none@none> |
added new option to documentation
|
| #
2109d469 |
|
30-Jan-2014 |
blanchet <none@none> |
renamed Sledgehammer options for symmetry between positive and negative versions
|
| #
0d4dda69 |
|
20-Jan-2014 |
blanchet <none@none> |
killed obsolete provers from documentation
|
| #
70e2710a |
|
19-Dec-2013 |
blanchet <none@none> |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
| #
965b3a7f |
|
17-Dec-2013 |
blanchet <none@none> |
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
|
| #
39268e77 |
|
08-Dec-2013 |
blanchet <none@none> |
added warning to documentation, based on isabelle-users thread
|
| #
e4c8fad6 |
|
17-Oct-2013 |
blanchet <none@none> |
added thread-safety warnings
|
| #
edc9b8a5 |
|
15-Oct-2013 |
blanchet <none@none> |
updated S/H docs
|
| #
e00e5a2e |
|
01-Oct-2013 |
blanchet <none@none> |
tiny doc fix
|
| #
af10c5fc |
|
23-Sep-2013 |
blanchet <none@none> |
document "spy" option
|
| #
9c9b1550 |
|
21-Sep-2013 |
wenzelm <none@none> |
repaired latex (cf. 7bb0cf27c243);
|
| #
55cfb0b2 |
|
20-Sep-2013 |
blanchet <none@none> |
document option
|
| #
b3d0bfe3 |
|
20-Sep-2013 |
blanchet <none@none> |
moved focus to Isabell/jEdit and away from Proof General
|
| #
e3d74f5a |
|
20-Sep-2013 |
blanchet <none@none> |
took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
|
| #
6515cc2d |
|
20-Sep-2013 |
blanchet <none@none> |
reduce the number of emitted MaSh commands (among others to facilitate debugging)
|
| #
38b14230 |
|
11-Sep-2013 |
blanchet <none@none> |
updated docs
|
| #
e31def9a |
|
28-Aug-2013 |
blanchet <none@none> |
tuned messages
|
| #
725d5d96 |
|
20-Aug-2013 |
blanchet <none@none> |
doc tuning
|
| #
e0b3c33d |
|
19-Aug-2013 |
blanchet <none@none> |
removed french option to manuals
|
| #
99c20780 |
|
13-Aug-2013 |
blanchet <none@none> |
updated Vampire version numbers
|
| #
0a6d4b13 |
|
29-Jul-2013 |
blanchet <none@none> |
updated Sledgehammer prover versions
|
| #
cac70bed |
|
20-May-2013 |
blanchet <none@none> |
updated Sledgehammer docs
|
| #
dc797756 |
|
20-Feb-2013 |
blanchet <none@none> |
upgraded to Alt-Ergo 0.95
|
| #
24cd411a |
|
20-Feb-2013 |
blanchet <none@none> |
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
|
| #
5be3a0be |
|
20-Feb-2013 |
blanchet <none@none> |
alias for people like me
|
| #
583ed312 |
|
14-Feb-2013 |
smolkas <none@none> |
renamed sledgehammer_shrink to sledgehammer_compress
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML => src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
|
| #
3c7e3d38 |
|
07-Feb-2013 |
blanchet <none@none> |
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
|
| #
b6be82e7 |
|
17-Jan-2013 |
blanchet <none@none> |
updated docs
|
| #
4f986899 |
|
04-Jan-2013 |
blanchet <none@none> |
updated docs
|
| #
f99d6679 |
|
11-Dec-2012 |
blanchet <none@none> |
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
|
| #
ae266679 |
|
10-Dec-2012 |
blanchet <none@none> |
changed capitalization of MeSh filter
|
| #
a373f201 |
|
25-Nov-2012 |
blanchet <none@none> |
updated MaSh doc
|
| #
33afc4e3 |
|
06-Nov-2012 |
blanchet <none@none> |
renamed Sledgehammer option
|
| #
10d1db30 |
|
18-Oct-2012 |
blanchet <none@none> |
updated docs
|
| #
a296c798 |
|
13-Sep-2012 |
blanchet <none@none> |
merged two commands
|
| #
ce7f2fdb |
|
28-Aug-2012 |
wenzelm <none@none> |
renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;
--HG--
rename : doc-src/Classes/Classes.thy => src/Doc/Classes/Classes.thy
rename : doc-src/Classes/Setup.thy => src/Doc/Classes/Setup.thy
rename : doc-src/Classes/document/build => src/Doc/Classes/document/build
rename : doc-src/Classes/document/root.tex => src/Doc/Classes/document/root.tex
rename : doc-src/Classes/document/style.sty => src/Doc/Classes/document/style.sty
rename : doc-src/Codegen/Adaptation.thy => src/Doc/Codegen/Adaptation.thy
rename : doc-src/Codegen/Evaluation.thy => src/Doc/Codegen/Evaluation.thy
rename : doc-src/Codegen/Foundations.thy => src/Doc/Codegen/Foundations.thy
rename : doc-src/Codegen/Further.thy => src/Doc/Codegen/Further.thy
rename : doc-src/Codegen/Inductive_Predicate.thy => src/Doc/Codegen/Inductive_Predicate.thy
rename : doc-src/Codegen/Introduction.thy => src/Doc/Codegen/Introduction.thy
rename : doc-src/Codegen/Refinement.thy => src/Doc/Codegen/Refinement.thy
rename : doc-src/Codegen/Setup.thy => src/Doc/Codegen/Setup.thy
rename : doc-src/Codegen/document/adapt.tex => src/Doc/Codegen/document/adapt.tex
rename : doc-src/Codegen/document/architecture.tex => src/Doc/Codegen/document/architecture.tex
rename : doc-src/Codegen/document/build => src/Doc/Codegen/document/build
rename : doc-src/Codegen/document/root.tex => src/Doc/Codegen/document/root.tex
rename : doc-src/Codegen/document/style.sty => src/Doc/Codegen/document/style.sty
rename : doc-src/Functions/Functions.thy => src/Doc/Functions/Functions.thy
rename : doc-src/Functions/document/build => src/Doc/Functions/document/build
rename : doc-src/Functions/document/conclusion.tex => src/Doc/Functions/document/conclusion.tex
rename : doc-src/Functions/document/intro.tex => src/Doc/Functions/document/intro.tex
rename : doc-src/Functions/document/mathpartir.sty => src/Doc/Functions/document/mathpartir.sty
rename : doc-src/Functions/document/root.tex => src/Doc/Functions/document/root.tex
rename : doc-src/Functions/document/style.sty => src/Doc/Functions/document/style.sty
rename : doc-src/HOL/document/HOL.tex => src/Doc/HOL/document/HOL.tex
rename : doc-src/HOL/document/build => src/Doc/HOL/document/build
rename : doc-src/HOL/document/root.tex => src/Doc/HOL/document/root.tex
rename : doc-src/Intro/document/advanced.tex => src/Doc/Intro/document/advanced.tex
rename : doc-src/Intro/document/build => src/Doc/Intro/document/build
rename : doc-src/Intro/document/foundations.tex => src/Doc/Intro/document/foundations.tex
rename : doc-src/Intro/document/getting.tex => src/Doc/Intro/document/getting.tex
rename : doc-src/Intro/document/root.tex => src/Doc/Intro/document/root.tex
rename : doc-src/IsarImplementation/Base.thy => src/Doc/IsarImplementation/Base.thy
rename : doc-src/IsarImplementation/Eq.thy => src/Doc/IsarImplementation/Eq.thy
rename : doc-src/IsarImplementation/Integration.thy => src/Doc/IsarImplementation/Integration.thy
rename : doc-src/IsarImplementation/Isar.thy => src/Doc/IsarImplementation/Isar.thy
rename : doc-src/IsarImplementation/Local_Theory.thy => src/Doc/IsarImplementation/Local_Theory.thy
rename : doc-src/IsarImplementation/Logic.thy => src/Doc/IsarImplementation/Logic.thy
rename : doc-src/IsarImplementation/ML.thy => src/Doc/IsarImplementation/ML.thy
rename : doc-src/IsarImplementation/Prelim.thy => src/Doc/IsarImplementation/Prelim.thy
rename : doc-src/IsarImplementation/Proof.thy => src/Doc/IsarImplementation/Proof.thy
rename : doc-src/IsarImplementation/Syntax.thy => src/Doc/IsarImplementation/Syntax.thy
rename : doc-src/IsarImplementation/Tactic.thy => src/Doc/IsarImplementation/Tactic.thy
rename : doc-src/IsarImplementation/document/build => src/Doc/IsarImplementation/document/build
rename : doc-src/IsarImplementation/document/root.tex => src/Doc/IsarImplementation/document/root.tex
rename : doc-src/IsarImplementation/document/style.sty => src/Doc/IsarImplementation/document/style.sty
rename : doc-src/IsarRef/Base.thy => src/Doc/IsarRef/Base.thy
rename : doc-src/IsarRef/Document_Preparation.thy => src/Doc/IsarRef/Document_Preparation.thy
rename : doc-src/IsarRef/First_Order_Logic.thy => src/Doc/IsarRef/First_Order_Logic.thy
rename : doc-src/IsarRef/Framework.thy => src/Doc/IsarRef/Framework.thy
rename : doc-src/IsarRef/Generic.thy => src/Doc/IsarRef/Generic.thy
rename : doc-src/IsarRef/HOL_Specific.thy => src/Doc/IsarRef/HOL_Specific.thy
rename : doc-src/IsarRef/Inner_Syntax.thy => src/Doc/IsarRef/Inner_Syntax.thy
rename : doc-src/IsarRef/ML_Tactic.thy => src/Doc/IsarRef/ML_Tactic.thy
rename : doc-src/IsarRef/Misc.thy => src/Doc/IsarRef/Misc.thy
rename : doc-src/IsarRef/Outer_Syntax.thy => src/Doc/IsarRef/Outer_Syntax.thy
rename : doc-src/IsarRef/Preface.thy => src/Doc/IsarRef/Preface.thy
rename : doc-src/IsarRef/Proof.thy => src/Doc/IsarRef/Proof.thy
rename : doc-src/IsarRef/Quick_Reference.thy => src/Doc/IsarRef/Quick_Reference.thy
rename : doc-src/IsarRef/Spec.thy => src/Doc/IsarRef/Spec.thy
rename : doc-src/IsarRef/Symbols.thy => src/Doc/IsarRef/Symbols.thy
rename : doc-src/IsarRef/Synopsis.thy => src/Doc/IsarRef/Synopsis.thy
rename : doc-src/IsarRef/document/build => src/Doc/IsarRef/document/build
rename : doc-src/IsarRef/document/isar-vm.eps => src/Doc/IsarRef/document/isar-vm.eps
rename : doc-src/IsarRef/document/isar-vm.pdf => src/Doc/IsarRef/document/isar-vm.pdf
rename : doc-src/IsarRef/document/isar-vm.svg => src/Doc/IsarRef/document/isar-vm.svg
rename : doc-src/IsarRef/document/root.tex => src/Doc/IsarRef/document/root.tex
rename : doc-src/IsarRef/document/showsymbols => src/Doc/IsarRef/document/showsymbols
rename : doc-src/IsarRef/document/style.sty => src/Doc/IsarRef/document/style.sty
rename : doc-src/LaTeXsugar/Sugar.thy => src/Doc/LaTeXsugar/Sugar.thy
rename : doc-src/LaTeXsugar/document/build => src/Doc/LaTeXsugar/document/build
rename : doc-src/LaTeXsugar/document/mathpartir.sty => src/Doc/LaTeXsugar/document/mathpartir.sty
rename : doc-src/LaTeXsugar/document/root.bib => src/Doc/LaTeXsugar/document/root.bib
rename : doc-src/LaTeXsugar/document/root.tex => src/Doc/LaTeXsugar/document/root.tex
rename : doc-src/Locales/Examples.thy => src/Doc/Locales/Examples.thy
rename : doc-src/Locales/Examples1.thy => src/Doc/Locales/Examples1.thy
rename : doc-src/Locales/Examples2.thy => src/Doc/Locales/Examples2.thy
rename : doc-src/Locales/Examples3.thy => src/Doc/Locales/Examples3.thy
rename : doc-src/Locales/document/build => src/Doc/Locales/document/build
rename : doc-src/Locales/document/root.bib => src/Doc/Locales/document/root.bib
rename : doc-src/Locales/document/root.tex => src/Doc/Locales/document/root.tex
rename : doc-src/Logics/abstract.txt => src/Doc/Logics/abstract.txt
rename : doc-src/Logics/document/CTT.tex => src/Doc/Logics/document/CTT.tex
rename : doc-src/Logics/document/LK.tex => src/Doc/Logics/document/LK.tex
rename : doc-src/Logics/document/Sequents.tex => src/Doc/Logics/document/Sequents.tex
rename : doc-src/Logics/document/build => src/Doc/Logics/document/build
rename : doc-src/Logics/document/preface.tex => src/Doc/Logics/document/preface.tex
rename : doc-src/Logics/document/root.tex => src/Doc/Logics/document/root.tex
rename : doc-src/Logics/document/syntax.tex => src/Doc/Logics/document/syntax.tex
rename : doc-src/Main/Main_Doc.thy => src/Doc/Main/Main_Doc.thy
rename : doc-src/Main/document/build => src/Doc/Main/document/build
rename : doc-src/Main/document/root.tex => src/Doc/Main/document/root.tex
rename : doc-src/Nitpick/document/build => src/Doc/Nitpick/document/build
rename : doc-src/Nitpick/document/root.tex => src/Doc/Nitpick/document/root.tex
rename : doc-src/ProgProve/Basics.thy => src/Doc/ProgProve/Basics.thy
rename : doc-src/ProgProve/Bool_nat_list.thy => src/Doc/ProgProve/Bool_nat_list.thy
rename : doc-src/ProgProve/Isar.thy => src/Doc/ProgProve/Isar.thy
rename : doc-src/ProgProve/LaTeXsugar.thy => src/Doc/ProgProve/LaTeXsugar.thy
rename : doc-src/ProgProve/Logic.thy => src/Doc/ProgProve/Logic.thy
rename : doc-src/ProgProve/MyList.thy => src/Doc/ProgProve/MyList.thy
rename : doc-src/ProgProve/Types_and_funs.thy => src/Doc/ProgProve/Types_and_funs.thy
rename : doc-src/ProgProve/document/bang.eps => src/Doc/ProgProve/document/bang.eps
rename : doc-src/ProgProve/document/bang.pdf => src/Doc/ProgProve/document/bang.pdf
rename : doc-src/ProgProve/document/build => src/Doc/ProgProve/document/build
rename : doc-src/ProgProve/document/intro-isabelle.tex => src/Doc/ProgProve/document/intro-isabelle.tex
rename : doc-src/ProgProve/document/mathpartir.sty => src/Doc/ProgProve/document/mathpartir.sty
rename : doc-src/ProgProve/document/prelude.tex => src/Doc/ProgProve/document/prelude.tex
rename : doc-src/ProgProve/document/root.bib => src/Doc/ProgProve/document/root.bib
rename : doc-src/ProgProve/document/root.tex => src/Doc/ProgProve/document/root.tex
rename : doc-src/ProgProve/document/svmono.cls => src/Doc/ProgProve/document/svmono.cls
rename : doc-src/ROOT => src/Doc/ROOT
rename : doc-src/Ref/abstract.txt => src/Doc/Ref/abstract.txt
rename : doc-src/Ref/document/build => src/Doc/Ref/document/build
rename : doc-src/Ref/document/classical.tex => src/Doc/Ref/document/classical.tex
rename : doc-src/Ref/document/root.tex => src/Doc/Ref/document/root.tex
rename : doc-src/Ref/document/simplifier.tex => src/Doc/Ref/document/simplifier.tex
rename : doc-src/Ref/document/substitution.tex => src/Doc/Ref/document/substitution.tex
rename : doc-src/Ref/document/syntax.tex => src/Doc/Ref/document/syntax.tex
rename : doc-src/Ref/document/tactic.tex => src/Doc/Ref/document/tactic.tex
rename : doc-src/Ref/document/thm.tex => src/Doc/Ref/document/thm.tex
rename : doc-src/Ref/undocumented.tex => src/Doc/Ref/undocumented.tex
rename : doc-src/Sledgehammer/document/build => src/Doc/Sledgehammer/document/build
rename : doc-src/Sledgehammer/document/root.tex => src/Doc/Sledgehammer/document/root.tex
rename : doc-src/System/Base.thy => src/Doc/System/Base.thy
rename : doc-src/System/Basics.thy => src/Doc/System/Basics.thy
rename : doc-src/System/Interfaces.thy => src/Doc/System/Interfaces.thy
rename : doc-src/System/Misc.thy => src/Doc/System/Misc.thy
rename : doc-src/System/Presentation.thy => src/Doc/System/Presentation.thy
rename : doc-src/System/Scala.thy => src/Doc/System/Scala.thy
rename : doc-src/System/Sessions.thy => src/Doc/System/Sessions.thy
rename : doc-src/System/document/browser_screenshot.eps => src/Doc/System/document/browser_screenshot.eps
rename : doc-src/System/document/browser_screenshot.png => src/Doc/System/document/browser_screenshot.png
rename : doc-src/System/document/build => src/Doc/System/document/build
rename : doc-src/System/document/root.tex => src/Doc/System/document/root.tex
rename : doc-src/TutorialI/Advanced/Partial.thy => src/Doc/Tutorial/Advanced/Partial.thy
rename : doc-src/TutorialI/Advanced/WFrec.thy => src/Doc/Tutorial/Advanced/WFrec.thy
rename : doc-src/TutorialI/Advanced/simp2.thy => src/Doc/Tutorial/Advanced/simp2.thy
rename : doc-src/TutorialI/CTL/Base.thy => src/Doc/Tutorial/CTL/Base.thy
rename : doc-src/TutorialI/CTL/CTL.thy => src/Doc/Tutorial/CTL/CTL.thy
rename : doc-src/TutorialI/CTL/CTLind.thy => src/Doc/Tutorial/CTL/CTLind.thy
rename : doc-src/TutorialI/CTL/PDL.thy => src/Doc/Tutorial/CTL/PDL.thy
rename : doc-src/TutorialI/CodeGen/CodeGen.thy => src/Doc/Tutorial/CodeGen/CodeGen.thy
rename : doc-src/TutorialI/Datatype/ABexpr.thy => src/Doc/Tutorial/Datatype/ABexpr.thy
rename : doc-src/TutorialI/Datatype/Fundata.thy => src/Doc/Tutorial/Datatype/Fundata.thy
rename : doc-src/TutorialI/Datatype/Nested.thy => src/Doc/Tutorial/Datatype/Nested.thy
rename : doc-src/TutorialI/Datatype/unfoldnested.thy => src/Doc/Tutorial/Datatype/unfoldnested.thy
rename : doc-src/TutorialI/Documents/Documents.thy => src/Doc/Tutorial/Documents/Documents.thy
rename : doc-src/TutorialI/Fun/fun0.thy => src/Doc/Tutorial/Fun/fun0.thy
rename : doc-src/TutorialI/Ifexpr/Ifexpr.thy => src/Doc/Tutorial/Ifexpr/Ifexpr.thy
rename : doc-src/TutorialI/Inductive/AB.thy => src/Doc/Tutorial/Inductive/AB.thy
rename : doc-src/TutorialI/Inductive/Advanced.thy => src/Doc/Tutorial/Inductive/Advanced.thy
rename : doc-src/TutorialI/Inductive/Even.thy => src/Doc/Tutorial/Inductive/Even.thy
rename : doc-src/TutorialI/Inductive/Mutual.thy => src/Doc/Tutorial/Inductive/Mutual.thy
rename : doc-src/TutorialI/Inductive/Star.thy => src/Doc/Tutorial/Inductive/Star.thy
rename : doc-src/TutorialI/Misc/AdvancedInd.thy => src/Doc/Tutorial/Misc/AdvancedInd.thy
rename : doc-src/TutorialI/Misc/Itrev.thy => src/Doc/Tutorial/Misc/Itrev.thy
rename : doc-src/TutorialI/Misc/Option2.thy => src/Doc/Tutorial/Misc/Option2.thy
rename : doc-src/TutorialI/Misc/Plus.thy => src/Doc/Tutorial/Misc/Plus.thy
rename : doc-src/TutorialI/Misc/Tree.thy => src/Doc/Tutorial/Misc/Tree.thy
rename : doc-src/TutorialI/Misc/Tree2.thy => src/Doc/Tutorial/Misc/Tree2.thy
rename : doc-src/TutorialI/Misc/appendix.thy => src/Doc/Tutorial/Misc/appendix.thy
rename : doc-src/TutorialI/Misc/case_exprs.thy => src/Doc/Tutorial/Misc/case_exprs.thy
rename : doc-src/TutorialI/Misc/fakenat.thy => src/Doc/Tutorial/Misc/fakenat.thy
rename : doc-src/TutorialI/Misc/natsum.thy => src/Doc/Tutorial/Misc/natsum.thy
rename : doc-src/TutorialI/Misc/pairs2.thy => src/Doc/Tutorial/Misc/pairs2.thy
rename : doc-src/TutorialI/Misc/prime_def.thy => src/Doc/Tutorial/Misc/prime_def.thy
rename : doc-src/TutorialI/Misc/simp.thy => src/Doc/Tutorial/Misc/simp.thy
rename : doc-src/TutorialI/Misc/types.thy => src/Doc/Tutorial/Misc/types.thy
rename : doc-src/TutorialI/Protocol/Event.thy => src/Doc/Tutorial/Protocol/Event.thy
rename : doc-src/TutorialI/Protocol/Message.thy => src/Doc/Tutorial/Protocol/Message.thy
rename : doc-src/TutorialI/Protocol/NS_Public.thy => src/Doc/Tutorial/Protocol/NS_Public.thy
rename : doc-src/TutorialI/Protocol/Public.thy => src/Doc/Tutorial/Protocol/Public.thy
rename : doc-src/TutorialI/Recdef/Induction.thy => src/Doc/Tutorial/Recdef/Induction.thy
rename : doc-src/TutorialI/Recdef/Nested0.thy => src/Doc/Tutorial/Recdef/Nested0.thy
rename : doc-src/TutorialI/Recdef/Nested1.thy => src/Doc/Tutorial/Recdef/Nested1.thy
rename : doc-src/TutorialI/Recdef/Nested2.thy => src/Doc/Tutorial/Recdef/Nested2.thy
rename : doc-src/TutorialI/Recdef/examples.thy => src/Doc/Tutorial/Recdef/examples.thy
rename : doc-src/TutorialI/Recdef/simplification.thy => src/Doc/Tutorial/Recdef/simplification.thy
rename : doc-src/TutorialI/Recdef/termination.thy => src/Doc/Tutorial/Recdef/termination.thy
rename : doc-src/TutorialI/Rules/Basic.thy => src/Doc/Tutorial/Rules/Basic.thy
rename : doc-src/TutorialI/Rules/Blast.thy => src/Doc/Tutorial/Rules/Blast.thy
rename : doc-src/TutorialI/Rules/Force.thy => src/Doc/Tutorial/Rules/Force.thy
rename : doc-src/TutorialI/Rules/Forward.thy => src/Doc/Tutorial/Rules/Forward.thy
rename : doc-src/TutorialI/Rules/Primes.thy => src/Doc/Tutorial/Rules/Primes.thy
rename : doc-src/TutorialI/Rules/Tacticals.thy => src/Doc/Tutorial/Rules/Tacticals.thy
rename : doc-src/TutorialI/Rules/find2.thy => src/Doc/Tutorial/Rules/find2.thy
rename : doc-src/TutorialI/Sets/Examples.thy => src/Doc/Tutorial/Sets/Examples.thy
rename : doc-src/TutorialI/Sets/Functions.thy => src/Doc/Tutorial/Sets/Functions.thy
rename : doc-src/TutorialI/Sets/Recur.thy => src/Doc/Tutorial/Sets/Recur.thy
rename : doc-src/TutorialI/Sets/Relations.thy => src/Doc/Tutorial/Sets/Relations.thy
rename : doc-src/TutorialI/ToyList/ToyList.thy => src/Doc/Tutorial/ToyList/ToyList.thy
rename : doc-src/TutorialI/ToyList/ToyList1 => src/Doc/Tutorial/ToyList/ToyList1
rename : doc-src/TutorialI/ToyList/ToyList2 => src/Doc/Tutorial/ToyList/ToyList2
rename : doc-src/TutorialI/Trie/Trie.thy => src/Doc/Tutorial/Trie/Trie.thy
rename : doc-src/TutorialI/Types/Axioms.thy => src/Doc/Tutorial/Types/Axioms.thy
rename : doc-src/TutorialI/Types/Numbers.thy => src/Doc/Tutorial/Types/Numbers.thy
rename : doc-src/TutorialI/Types/Overloading.thy => src/Doc/Tutorial/Types/Overloading.thy
rename : doc-src/TutorialI/Types/Pairs.thy => src/Doc/Tutorial/Types/Pairs.thy
rename : doc-src/TutorialI/Types/Records.thy => src/Doc/Tutorial/Types/Records.thy
rename : doc-src/TutorialI/Types/Setup.thy => src/Doc/Tutorial/Types/Setup.thy
rename : doc-src/TutorialI/Types/Typedefs.thy => src/Doc/Tutorial/Types/Typedefs.thy
rename : doc-src/TutorialI/document/Isa-logics.eps => src/Doc/Tutorial/document/Isa-logics.eps
rename : doc-src/TutorialI/document/Isa-logics.pdf => src/Doc/Tutorial/document/Isa-logics.pdf
rename : doc-src/TutorialI/document/advanced0.tex => src/Doc/Tutorial/document/advanced0.tex
rename : doc-src/TutorialI/document/appendix0.tex => src/Doc/Tutorial/document/appendix0.tex
rename : doc-src/TutorialI/document/basics.tex => src/Doc/Tutorial/document/basics.tex
rename : doc-src/TutorialI/document/build => src/Doc/Tutorial/document/build
rename : doc-src/TutorialI/document/cl2emono-modified.sty => src/Doc/Tutorial/document/cl2emono-modified.sty
rename : doc-src/TutorialI/document/ctl0.tex => src/Doc/Tutorial/document/ctl0.tex
rename : doc-src/TutorialI/document/documents0.tex => src/Doc/Tutorial/document/documents0.tex
rename : doc-src/TutorialI/document/fp.tex => src/Doc/Tutorial/document/fp.tex
rename : doc-src/TutorialI/document/inductive0.tex => src/Doc/Tutorial/document/inductive0.tex
rename : doc-src/TutorialI/document/isa-index => src/Doc/Tutorial/document/isa-index
rename : doc-src/TutorialI/document/numerics.tex => src/Doc/Tutorial/document/numerics.tex
rename : doc-src/TutorialI/document/pghead.eps => src/Doc/Tutorial/document/pghead.eps
rename : doc-src/TutorialI/document/pghead.pdf => src/Doc/Tutorial/document/pghead.pdf
rename : doc-src/TutorialI/document/preface.tex => src/Doc/Tutorial/document/preface.tex
rename : doc-src/TutorialI/document/protocol.tex => src/Doc/Tutorial/document/protocol.tex
rename : doc-src/TutorialI/document/root.tex => src/Doc/Tutorial/document/root.tex
rename : doc-src/TutorialI/document/rules.tex => src/Doc/Tutorial/document/rules.tex
rename : doc-src/TutorialI/document/sets.tex => src/Doc/Tutorial/document/sets.tex
rename : doc-src/TutorialI/document/tutorial.sty => src/Doc/Tutorial/document/tutorial.sty
rename : doc-src/TutorialI/document/typedef.pdf => src/Doc/Tutorial/document/typedef.pdf
rename : doc-src/TutorialI/document/typedef.ps => src/Doc/Tutorial/document/typedef.ps
rename : doc-src/TutorialI/document/types0.tex => src/Doc/Tutorial/document/types0.tex
rename : doc-src/TutorialI/todo.tobias => src/Doc/Tutorial/todo.tobias
rename : doc-src/ZF/FOL_examples.thy => src/Doc/ZF/FOL_examples.thy
rename : doc-src/ZF/IFOL_examples.thy => src/Doc/ZF/IFOL_examples.thy
rename : doc-src/ZF/If.thy => src/Doc/ZF/If.thy
rename : doc-src/ZF/ZF_Isar.thy => src/Doc/ZF/ZF_Isar.thy
rename : doc-src/ZF/ZF_examples.thy => src/Doc/ZF/ZF_examples.thy
rename : doc-src/ZF/document/FOL.tex => src/Doc/ZF/document/FOL.tex
rename : doc-src/ZF/document/ZF.tex => src/Doc/ZF/document/ZF.tex
rename : doc-src/ZF/document/build => src/Doc/ZF/document/build
rename : doc-src/ZF/document/logics.sty => src/Doc/ZF/document/logics.sty
rename : doc-src/ZF/document/root.tex => src/Doc/ZF/document/root.tex
rename : doc-src/antiquote_setup.ML => src/Doc/antiquote_setup.ML
rename : doc-src/extra.sty => src/Doc/extra.sty
rename : doc-src/fixbookmarks => src/Doc/fixbookmarks
rename : doc-src/iman.sty => src/Doc/iman.sty
rename : doc-src/isar.sty => src/Doc/isar.sty
rename : doc-src/manual.bib => src/Doc/manual.bib
rename : doc-src/mathsing.sty => src/Doc/mathsing.sty
rename : doc-src/more_antiquote.ML => src/Doc/more_antiquote.ML
rename : doc-src/pdfsetup.sty => src/Doc/pdfsetup.sty
rename : doc-src/preface.tex => src/Doc/preface.tex
rename : doc-src/prepare_document => src/Doc/prepare_document
rename : doc-src/proof.sty => src/Doc/proof.sty
rename : doc-src/sedindex => src/Doc/sedindex
rename : doc-src/ttbox.sty => src/Doc/ttbox.sty
rename : doc-src/underscore.sty => src/Doc/underscore.sty
|