| #
0ac75c50 |
|
22-Jul-2018 |
eberlm <eberlm@in.tum.de> |
Moved Real_Asymp manual
--HG--
extra : rebase_source : 5fd5a6b02d4ec9505df08e71b20e95bad1013e05
|
| #
6985f7d6 |
|
15-Jul-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Added Real_Asymp package
|
| #
f90bf366 |
|
19-Mar-2018 |
wenzelm <none@none> |
documentation for the Isabelle server;
|
| #
c11192ba |
|
16-Dec-2017 |
wenzelm <none@none> |
added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
|
| #
dd1da728 |
|
16-Dec-2017 |
wenzelm <none@none> |
PIDE markup for session ROOT files;
|
| #
79d1d0f9 |
|
06-Dec-2017 |
wenzelm <none@none> |
just one session for bulky HOL-Analysis documents;
|
| #
d3fe6079 |
|
06-Dec-2017 |
nipkow <none@none> |
initial version of Analysis document
|
| #
5e9b9c3a |
|
31-Oct-2017 |
wenzelm <none@none> |
clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
|
| #
443eb83f |
|
30-Oct-2017 |
wenzelm <none@none> |
ROOT cleanup: empty 'document_files' means there is no document;
|
| #
8754266b |
|
02-Oct-2017 |
wenzelm <none@none> |
eliminated old-style no-document imports;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
8a77dcf6 |
|
17-Aug-2017 |
wenzelm <none@none> |
clarified imports;
|
| #
a6e39efc |
|
24-Apr-2017 |
wenzelm <none@none> |
clarified parent session images, to avoid duplicate loading of theories;
|
| #
e6717aed |
|
23-Apr-2017 |
wenzelm <none@none> |
clarified parent session images, to avoid duplicate loading of theories;
|
| #
84d89437 |
|
22-Feb-2017 |
haftmann <none@none> |
basic documentation for computations
--HG--
extra : rebase_source : d93164fed6eb40c0d78779f72878f42feb87415b
|
| #
630d7da8 |
|
20-Nov-2016 |
wenzelm <none@none> |
more on "Formal scopes and semantic selection";
|
| #
935dd413 |
|
18-Apr-2016 |
haftmann <none@none> |
fragment of a HOL type class primer
--HG--
extra : rebase_source : c7ff6bceea8256c21b8b1f6081b53aad1df6c942
|
| #
010f2dee |
|
29-Mar-2016 |
blanchet <none@none> |
added sketchy 'corec' documentation
|
| #
16cd6d0e |
|
16-Mar-2016 |
wenzelm <none@none> |
clarified name;
--HG--
rename : src/Doc/System/Basics.thy => src/Doc/System/Environment.thy
|
| #
a8a49489 |
|
19-Feb-2016 |
wenzelm <none@none> |
moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
|
| #
0d72d301 |
|
17-Feb-2016 |
wenzelm <none@none> |
SML/NJ is no longer supported;
|
| #
7c773591 |
|
24-Jan-2016 |
wenzelm <none@none> |
guard sessions that no longer work with SML/NJ -- memory problems;
|
| #
e6603a15 |
|
12-Jan-2016 |
wenzelm <none@none> |
updated old screenshots, added new screenshots;
|
| #
0b85b81d |
|
31-Dec-2015 |
wenzelm <none@none> |
discontinued documentation of old browser;
tuned;
|
| #
287d33fa |
|
06-Jul-2015 |
wenzelm <none@none> |
clarified sections;
|
| #
c68b1d67 |
|
06-Jul-2015 |
wenzelm <none@none> |
removed outdated and mostly obsolete material;
|
| #
fccbd5ff |
|
15-Jun-2015 |
wenzelm <none@none> |
moved sections;
|
| #
4aaf661f |
|
19-May-2015 |
wenzelm <none@none> |
more on displays with very high resolution;
|
| #
2a31bd88 |
|
17-May-2015 |
wenzelm <none@none> |
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
|
| #
9688338f |
|
04-May-2015 |
wenzelm <none@none> |
more on Isabelle document preparation and bibtex files;
|
| #
ee31fcb5 |
|
19-Jan-2015 |
wenzelm <none@none> |
no document here;
|
| #
52182cff |
|
15-Jan-2015 |
haftmann <none@none> |
separate image for prerequisites of codegen tutorial
--HG--
extra : rebase_source : c5c16c7f698cac43259b606eaa507dfb6ee3028c
|
| #
8c11536a |
|
22-Dec-2014 |
wenzelm <none@none> |
system option "pretty_margin" is superseded by "thy_output_margin";
|
| #
eec5492d |
|
28-Oct-2014 |
wenzelm <none@none> |
'notepad' requires proper nesting of begin/end;
|
| #
fb2f6a3a |
|
01-Sep-2014 |
blanchet <none@none> |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
|
| #
90bfe9e5 |
|
26-Jun-2014 |
wenzelm <none@none> |
suppress documentation "how_to_prove_it" for now, notably for release;
|
| #
60c1a868 |
|
18-Jun-2014 |
wenzelm <none@none> |
added screenshot;
--HG--
extra : rebase_source : 5f974dca4bd9f6cfd87874ada166c8756c8ea9c9
|
| #
efda2282 |
|
17-Jun-2014 |
wenzelm <none@none> |
added screenshot;
--HG--
extra : rebase_source : b62e8b56002dcd8d53fbdc58db8b543c10c12a4d
|
| #
9c7a2ba2 |
|
15-Jun-2014 |
wenzelm <none@none> |
clarified role of old user interfaces as misc tools;
--HG--
extra : rebase_source : 5764882fd3e1f09e1ca95f448011e97f6cb4218f
|
| #
aeec33a6 |
|
05-Jun-2014 |
wenzelm <none@none> |
updated screenshots;
--HG--
extra : rebase_source : 6870775642fd3dc1b2d2c8d2348ce5bbc5f9b340
|
| #
aff4c530 |
|
24-May-2014 |
wenzelm <none@none> |
more portable file names;
--HG--
rename : src/Doc/Tutorial/ToyList/ToyList1 => src/Doc/Tutorial/ToyList/ToyList1.txt
rename : src/Doc/Tutorial/ToyList/ToyList2 => src/Doc/Tutorial/ToyList/ToyList2.txt
|
| #
d48f7aae |
|
02-May-2014 |
wenzelm <none@none> |
more standard doc session specification;
|
| #
b92e784f |
|
10-Apr-2014 |
wenzelm <none@none> |
more formal dependencies via 'document_files';
|
| #
96971814 |
|
07-Apr-2014 |
haftmann <none@none> |
even more standardized doc session names after #b266e7a86485
--HG--
rename : src/Doc/Isar-Ref/Base.thy => src/Doc/Isar_Ref/Base.thy
rename : src/Doc/Isar-Ref/Document_Preparation.thy => src/Doc/Isar_Ref/Document_Preparation.thy
rename : src/Doc/Isar-Ref/First_Order_Logic.thy => src/Doc/Isar_Ref/First_Order_Logic.thy
rename : src/Doc/Isar-Ref/Framework.thy => src/Doc/Isar_Ref/Framework.thy
rename : src/Doc/Isar-Ref/Generic.thy => src/Doc/Isar_Ref/Generic.thy
rename : src/Doc/Isar-Ref/HOL_Specific.thy => src/Doc/Isar_Ref/HOL_Specific.thy
rename : src/Doc/Isar-Ref/Inner_Syntax.thy => src/Doc/Isar_Ref/Inner_Syntax.thy
rename : src/Doc/Isar-Ref/ML_Tactic.thy => src/Doc/Isar_Ref/ML_Tactic.thy
rename : src/Doc/Isar-Ref/Misc.thy => src/Doc/Isar_Ref/Misc.thy
rename : src/Doc/Isar-Ref/Outer_Syntax.thy => src/Doc/Isar_Ref/Outer_Syntax.thy
rename : src/Doc/Isar-Ref/Preface.thy => src/Doc/Isar_Ref/Preface.thy
rename : src/Doc/Isar-Ref/Proof.thy => src/Doc/Isar_Ref/Proof.thy
rename : src/Doc/Isar-Ref/Quick_Reference.thy => src/Doc/Isar_Ref/Quick_Reference.thy
rename : src/Doc/Isar-Ref/Spec.thy => src/Doc/Isar_Ref/Spec.thy
rename : src/Doc/Isar-Ref/Symbols.thy => src/Doc/Isar_Ref/Symbols.thy
rename : src/Doc/Isar-Ref/Synopsis.thy => src/Doc/Isar_Ref/Synopsis.thy
rename : src/Doc/Isar-Ref/document/build => src/Doc/Isar_Ref/document/build
rename : src/Doc/Isar-Ref/document/isar-vm.pdf => src/Doc/Isar_Ref/document/isar-vm.pdf
rename : src/Doc/Isar-Ref/document/isar-vm.svg => src/Doc/Isar_Ref/document/isar-vm.svg
rename : src/Doc/Isar-Ref/document/root.tex => src/Doc/Isar_Ref/document/root.tex
rename : src/Doc/Isar-Ref/document/showsymbols => src/Doc/Isar_Ref/document/showsymbols
rename : src/Doc/Isar-Ref/document/style.sty => src/Doc/Isar_Ref/document/style.sty
rename : src/Doc/Logics-ZF/FOL_examples.thy => src/Doc/Logics_ZF/FOL_examples.thy
rename : src/Doc/Logics-ZF/IFOL_examples.thy => src/Doc/Logics_ZF/IFOL_examples.thy
rename : src/Doc/Logics-ZF/If.thy => src/Doc/Logics_ZF/If.thy
rename : src/Doc/Logics-ZF/ZF_Isar.thy => src/Doc/Logics_ZF/ZF_Isar.thy
rename : src/Doc/Logics-ZF/ZF_examples.thy => src/Doc/Logics_ZF/ZF_examples.thy
rename : src/Doc/Logics-ZF/document/FOL.tex => src/Doc/Logics_ZF/document/FOL.tex
rename : src/Doc/Logics-ZF/document/ZF.tex => src/Doc/Logics_ZF/document/ZF.tex
rename : src/Doc/Logics-ZF/document/build => src/Doc/Logics_ZF/document/build
rename : src/Doc/Logics-ZF/document/logics.sty => src/Doc/Logics_ZF/document/logics.sty
rename : src/Doc/Logics-ZF/document/root.tex => src/Doc/Logics_ZF/document/root.tex
rename : src/Doc/Prog-Prove/Basics.thy => src/Doc/Prog_Prove/Basics.thy
rename : src/Doc/Prog-Prove/Bool_nat_list.thy => src/Doc/Prog_Prove/Bool_nat_list.thy
rename : src/Doc/Prog-Prove/Isar.thy => src/Doc/Prog_Prove/Isar.thy
rename : src/Doc/Prog-Prove/LaTeXsugar.thy => src/Doc/Prog_Prove/LaTeXsugar.thy
rename : src/Doc/Prog-Prove/Logic.thy => src/Doc/Prog_Prove/Logic.thy
rename : src/Doc/Prog-Prove/MyList.thy => src/Doc/Prog_Prove/MyList.thy
rename : src/Doc/Prog-Prove/Types_and_funs.thy => src/Doc/Prog_Prove/Types_and_funs.thy
rename : src/Doc/Prog-Prove/document/bang.pdf => src/Doc/Prog_Prove/document/bang.pdf
rename : src/Doc/Prog-Prove/document/build => src/Doc/Prog_Prove/document/build
rename : src/Doc/Prog-Prove/document/intro-isabelle.tex => src/Doc/Prog_Prove/document/intro-isabelle.tex
rename : src/Doc/Prog-Prove/document/mathpartir.sty => src/Doc/Prog_Prove/document/mathpartir.sty
rename : src/Doc/Prog-Prove/document/prelude.tex => src/Doc/Prog_Prove/document/prelude.tex
rename : src/Doc/Prog-Prove/document/root.bib => src/Doc/Prog_Prove/document/root.bib
rename : src/Doc/Prog-Prove/document/root.tex => src/Doc/Prog_Prove/document/root.tex
rename : src/Doc/Prog-Prove/document/svmono.cls => src/Doc/Prog_Prove/document/svmono.cls
|
| #
3b42617a |
|
05-Apr-2014 |
haftmann <none@none> |
closer correspondence of document and session names, while maintaining document names for external reference
--HG--
rename : src/Doc/IsarImplementation/Base.thy => src/Doc/Implementation/Base.thy
rename : src/Doc/IsarImplementation/Eq.thy => src/Doc/Implementation/Eq.thy
rename : src/Doc/IsarImplementation/Integration.thy => src/Doc/Implementation/Integration.thy
rename : src/Doc/IsarImplementation/Isar.thy => src/Doc/Implementation/Isar.thy
rename : src/Doc/IsarImplementation/Local_Theory.thy => src/Doc/Implementation/Local_Theory.thy
rename : src/Doc/IsarImplementation/Logic.thy => src/Doc/Implementation/Logic.thy
rename : src/Doc/IsarImplementation/ML.thy => src/Doc/Implementation/ML.thy
rename : src/Doc/IsarImplementation/Prelim.thy => src/Doc/Implementation/Prelim.thy
rename : src/Doc/IsarImplementation/Proof.thy => src/Doc/Implementation/Proof.thy
rename : src/Doc/IsarImplementation/Syntax.thy => src/Doc/Implementation/Syntax.thy
rename : src/Doc/IsarImplementation/Tactic.thy => src/Doc/Implementation/Tactic.thy
rename : src/Doc/IsarImplementation/document/build => src/Doc/Implementation/document/build
rename : src/Doc/IsarImplementation/document/root.tex => src/Doc/Implementation/document/root.tex
rename : src/Doc/IsarImplementation/document/style.sty => src/Doc/Implementation/document/style.sty
rename : src/Doc/IsarRef/Base.thy => src/Doc/Isar-Ref/Base.thy
rename : src/Doc/IsarRef/Document_Preparation.thy => src/Doc/Isar-Ref/Document_Preparation.thy
rename : src/Doc/IsarRef/First_Order_Logic.thy => src/Doc/Isar-Ref/First_Order_Logic.thy
rename : src/Doc/IsarRef/Framework.thy => src/Doc/Isar-Ref/Framework.thy
rename : src/Doc/IsarRef/Generic.thy => src/Doc/Isar-Ref/Generic.thy
rename : src/Doc/IsarRef/HOL_Specific.thy => src/Doc/Isar-Ref/HOL_Specific.thy
rename : src/Doc/IsarRef/Inner_Syntax.thy => src/Doc/Isar-Ref/Inner_Syntax.thy
rename : src/Doc/IsarRef/ML_Tactic.thy => src/Doc/Isar-Ref/ML_Tactic.thy
rename : src/Doc/IsarRef/Misc.thy => src/Doc/Isar-Ref/Misc.thy
rename : src/Doc/IsarRef/Outer_Syntax.thy => src/Doc/Isar-Ref/Outer_Syntax.thy
rename : src/Doc/IsarRef/Preface.thy => src/Doc/Isar-Ref/Preface.thy
rename : src/Doc/IsarRef/Proof.thy => src/Doc/Isar-Ref/Proof.thy
rename : src/Doc/IsarRef/Quick_Reference.thy => src/Doc/Isar-Ref/Quick_Reference.thy
rename : src/Doc/IsarRef/Spec.thy => src/Doc/Isar-Ref/Spec.thy
rename : src/Doc/IsarRef/Symbols.thy => src/Doc/Isar-Ref/Symbols.thy
rename : src/Doc/IsarRef/Synopsis.thy => src/Doc/Isar-Ref/Synopsis.thy
rename : src/Doc/IsarRef/document/build => src/Doc/Isar-Ref/document/build
rename : src/Doc/IsarRef/document/isar-vm.pdf => src/Doc/Isar-Ref/document/isar-vm.pdf
rename : src/Doc/IsarRef/document/isar-vm.svg => src/Doc/Isar-Ref/document/isar-vm.svg
rename : src/Doc/IsarRef/document/root.tex => src/Doc/Isar-Ref/document/root.tex
rename : src/Doc/IsarRef/document/showsymbols => src/Doc/Isar-Ref/document/showsymbols
rename : src/Doc/IsarRef/document/style.sty => src/Doc/Isar-Ref/document/style.sty
rename : src/Doc/ZF/FOL_examples.thy => src/Doc/Logics-ZF/FOL_examples.thy
rename : src/Doc/ZF/IFOL_examples.thy => src/Doc/Logics-ZF/IFOL_examples.thy
rename : src/Doc/ZF/If.thy => src/Doc/Logics-ZF/If.thy
rename : src/Doc/ZF/ZF_Isar.thy => src/Doc/Logics-ZF/ZF_Isar.thy
rename : src/Doc/ZF/ZF_examples.thy => src/Doc/Logics-ZF/ZF_examples.thy
rename : src/Doc/ZF/document/FOL.tex => src/Doc/Logics-ZF/document/FOL.tex
rename : src/Doc/ZF/document/ZF.tex => src/Doc/Logics-ZF/document/ZF.tex
rename : src/Doc/ZF/document/build => src/Doc/Logics-ZF/document/build
rename : src/Doc/ZF/document/logics.sty => src/Doc/Logics-ZF/document/logics.sty
rename : src/Doc/ZF/document/root.tex => src/Doc/Logics-ZF/document/root.tex
rename : src/Doc/ProgProve/Basics.thy => src/Doc/Prog-Prove/Basics.thy
rename : src/Doc/ProgProve/Bool_nat_list.thy => src/Doc/Prog-Prove/Bool_nat_list.thy
rename : src/Doc/ProgProve/Isar.thy => src/Doc/Prog-Prove/Isar.thy
rename : src/Doc/ProgProve/LaTeXsugar.thy => src/Doc/Prog-Prove/LaTeXsugar.thy
rename : src/Doc/ProgProve/Logic.thy => src/Doc/Prog-Prove/Logic.thy
rename : src/Doc/ProgProve/MyList.thy => src/Doc/Prog-Prove/MyList.thy
rename : src/Doc/ProgProve/Types_and_funs.thy => src/Doc/Prog-Prove/Types_and_funs.thy
rename : src/Doc/ProgProve/document/bang.pdf => src/Doc/Prog-Prove/document/bang.pdf
rename : src/Doc/ProgProve/document/build => src/Doc/Prog-Prove/document/build
rename : src/Doc/ProgProve/document/intro-isabelle.tex => src/Doc/Prog-Prove/document/intro-isabelle.tex
rename : src/Doc/ProgProve/document/mathpartir.sty => src/Doc/Prog-Prove/document/mathpartir.sty
rename : src/Doc/ProgProve/document/prelude.tex => src/Doc/Prog-Prove/document/prelude.tex
rename : src/Doc/ProgProve/document/root.bib => src/Doc/Prog-Prove/document/root.bib
rename : src/Doc/ProgProve/document/root.tex => src/Doc/Prog-Prove/document/root.tex
rename : src/Doc/ProgProve/document/svmono.cls => src/Doc/Prog-Prove/document/svmono.cls
rename : src/Doc/LaTeXsugar/Sugar.thy => src/Doc/Sugar/Sugar.thy
rename : src/Doc/LaTeXsugar/document/build => src/Doc/Sugar/document/build
rename : src/Doc/LaTeXsugar/document/mathpartir.sty => src/Doc/Sugar/document/mathpartir.sty
rename : src/Doc/LaTeXsugar/document/root.bib => src/Doc/Sugar/document/root.bib
rename : src/Doc/LaTeXsugar/document/root.tex => src/Doc/Sugar/document/root.tex
extra : rebase_source : dcaca23a302f6dfe8e8c7fc25da164e0e596751b
|
| #
3fd6cc4a |
|
10-Feb-2014 |
wenzelm <none@none> |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
| #
0ab6fc18 |
|
28-Jan-2014 |
paulson <lp15@cam.ac.uk> |
Replacing the theory Library/Binomial by Number_Theory/Binomial
--HG--
rename : src/Doc/Tutorial/Rules/Primes.thy => src/Doc/Tutorial/Rules/TPrimes.thy
|
| #
098b5d30 |
|
20-Jan-2014 |
blanchet <none@none> |
reduced dependencies + updated docs
|
| #
fa797403 |
|
31-Oct-2013 |
wenzelm <none@none> |
more on automatically tried tools;
|
| #
40817214 |
|
12-Oct-2013 |
wenzelm <none@none> |
more screenshots;
tuned;
|
| #
60d4134a |
|
01-Oct-2013 |
krauss <none@none> |
basic documentation for function elimination rules and fun_cases
--HG--
extra : source : 0053bdc3dd3e925f1ac13ff6e5e6136ed7b9e6f1
|
| #
f736ecb8 |
|
21-Sep-2013 |
wenzelm <none@none> |
basic setup for Isabelle/jEdit documentation;
|
| #
b3c5081c |
|
13-Sep-2013 |
blanchet <none@none> |
removed accidentally submitted line
|
| #
6ac6a2de |
|
13-Sep-2013 |
blanchet <none@none> |
more (co)data doc
|
| #
6bca411e |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
ee30348a |
|
11-Sep-2013 |
blanchet <none@none> |
more (co)data docs
|
| #
62659e09 |
|
03-Sep-2013 |
wenzelm <none@none> |
more robust ToyList_Test;
|
| #
3088ce6b |
|
01-Aug-2013 |
blanchet <none@none> |
more (co)datatype docs
|
| #
0d770f06 |
|
30-Jul-2013 |
blanchet <none@none> |
sketched documentation for new (co)datatype package
|
| #
0ee1ebab |
|
27-Jul-2013 |
wenzelm <none@none> |
more direct inclusion of tikz pictures;
|
| #
db3363bd |
|
27-Jul-2013 |
wenzelm <none@none> |
obsolete;
|
| #
7b569724 |
|
07-Jul-2013 |
wenzelm <none@none> |
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
--HG--
rename : src/Doc/HOL/document/HOL.tex => src/Doc/Logics/document/HOL.tex
|
| #
709e149c |
|
02-Jul-2013 |
wenzelm <none@none> |
clarified Proofterm.proofs vs. Goal.skip_proofs;
|
| #
d2193df8 |
|
29-Jun-2013 |
wenzelm <none@none> |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
discontinued unused proofterms for FOL;
|
| #
deb713c1 |
|
25-Jun-2013 |
wenzelm <none@none> |
more robust options, notably for isatest mac-poly-M8-skip_proofs;
|
| #
855be9d9 |
|
18-Jun-2013 |
wenzelm <none@none> |
eliminated old "ref" manual;
--HG--
extra : rebase_source : 62182fbdafa35f9b33a6218abc747b6f59126d44
|
| #
a04ca5fd |
|
18-Jun-2013 |
wenzelm <none@none> |
more on built-in syntax transformations, based on reduced version of old material;
--HG--
extra : rebase_source : ce6356a3bf2f2622e8fa13e6bd877ac8ff3081b1
|
| #
c21168ca |
|
17-Jun-2013 |
wenzelm <none@none> |
more on concrete syntax of proof terms;
--HG--
extra : rebase_source : cd9449d5e666a8454d237a06f8418d68afea1ced
|
| #
cd2ee02e |
|
17-Jun-2013 |
wenzelm <none@none> |
more examples on proof terms;
--HG--
extra : rebase_source : 1078d49035d7ae02424adfdc0759eb22a9f25d01
|
| #
51d94d7f |
|
27-Mar-2013 |
wenzelm <none@none> |
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
|
| #
34905e00 |
|
11-Mar-2013 |
wenzelm <none@none> |
support for 'chapter' specifications within session ROOT;
|
| #
3d4c9173 |
|
07-Dec-2012 |
wenzelm <none@none> |
eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
\usepackage{proof} only where required;
|
| #
fef8498a |
|
12-Nov-2012 |
wenzelm <none@none> |
removed somewhat pointless historic material;
--HG--
extra : rebase_source : 75ba626f499df5057dceb7aa4ce78be2001d6ada
|
| #
eb3c8137 |
|
11-Nov-2012 |
wenzelm <none@none> |
updated section on ordered rewriting;
--HG--
extra : rebase_source : 05c0aa1a8a6ae7ac5d69b0d98bde3ce14ba9402d
|
| #
24d8f4fe |
|
07-Nov-2012 |
wenzelm <none@none> |
some coverage of "resolution without lifting", which should be normally avoided;
--HG--
extra : rebase_source : 08dbf1b964703b18468737b11c04a1746873d67b
|
| #
4b171929 |
|
06-Nov-2012 |
wenzelm <none@none> |
moved classical wrappers to IsarRef;
removed somewhat pointless historic material;
--HG--
extra : rebase_source : 15ca7698b888d40293c3e99c2d3e2efbac7fac58
|
| #
6cab4831 |
|
12-Sep-2012 |
wenzelm <none@none> |
some attempts to synchronize ROOT/files and document/build;
|
| #
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
|