| #
8413f38b |
|
22-Jun-2018 |
wenzelm <none@none> |
clarified document antiquotation @{theory};
|
| #
515bdf02 |
|
14-Dec-2017 |
haftmann <none@none> |
dedicated case option for code generation to Scala
--HG--
extra : rebase_source : f4d2da47982250c33b66f81d009da3f3d0b48bbd
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
9322bd71 |
|
02-Jul-2017 |
haftmann <none@none> |
proper concept of code declaration wrt. atomicity and Isar declarations
--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472
|
| #
8a89ac2e |
|
31-May-2017 |
wenzelm <none@none> |
more robust -- avoid race condition wrt. Haskell output in $ISABELLE_TMP/examples/
|
| #
84d89437 |
|
22-Feb-2017 |
haftmann <none@none> |
basic documentation for computations
--HG--
extra : rebase_source : d93164fed6eb40c0d78779f72878f42feb87415b
|
| #
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
| #
37b50607 |
|
11-Aug-2016 |
wenzelm <none@none> |
clarified antiquotations;
|
| #
1a3088a0 |
|
14-Jun-2016 |
haftmann <none@none> |
explicit resolution of ambiguous dictionaries
|
| #
c751372b |
|
06-Jun-2016 |
haftmann <none@none> |
tuned signature
--HG--
extra : rebase_source : 929e17c758c4a9f52dc18071df8bf63d5fbb7675
|
| #
2e392e73 |
|
06-Jun-2016 |
haftmann <none@none> |
explicit tagging of code equations de-baroquifies interface
--HG--
extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655
|
| #
a424472e |
|
19-Dec-2015 |
haftmann <none@none> |
documentation on last state of the art concerning interpretation
|
| #
90db10ea |
|
03-Dec-2015 |
haftmann <none@none> |
consolidated documentation
|
| #
b2dfeb3f |
|
14-Nov-2015 |
haftmann <none@none> |
prefer "rewrites" and "defines" to note rewrite morphisms
--HG--
extra : rebase_source : db946849cc605955aa705d31965275c62fa42379
|
| #
be94c509 |
|
14-Nov-2015 |
haftmann <none@none> |
coalesce permanent_interpretation.ML with interpretation.ML
--HG--
extra : rebase_source : 580d89700ffeaf7aa823f4bcc4e638cca8ce081d
|
| #
8e8b881c |
|
04-Nov-2015 |
ballarin <none@none> |
Keyword 'rewrites' identifies rewrite morphisms.
|
| #
52182cff |
|
15-Jan-2015 |
haftmann <none@none> |
separate image for prerequisites of codegen tutorial
--HG--
extra : rebase_source : c5c16c7f698cac43259b606eaa507dfb6ee3028c
|
| #
4b214c04 |
|
15-Jan-2015 |
haftmann <none@none> |
modernized cartouches
--HG--
extra : rebase_source : 412f72526ed2ebf94539b64f7bd1b531dc7c349a
|
| #
fdba2893 |
|
14-Nov-2014 |
haftmann <none@none> |
documentation stubs about permanent_interpretation
--HG--
extra : rebase_source : cbe41a8799c0dc8caf5eea7c08225f6babfc4296
|
| #
a1f39138 |
|
07-Oct-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
e41a1507 |
|
26-Feb-2014 |
haftmann <none@none> |
prefer proof context over background theory
--HG--
extra : rebase_source : 307a2e54d5c0b89d8668ce99110df0538037668e
|
| #
f0637e3a |
|
09-Feb-2014 |
haftmann <none@none> |
dropped legacy finally
--HG--
extra : rebase_source : cc3d5b4eeefa467c96b4dd3e4a72a54b2c6b9f95
|
| #
1d1fac2a |
|
15-Jul-2013 |
wenzelm <none@none> |
prefer @{file} references that are actually checked;
|
| #
38f6cafa |
|
15-Jun-2013 |
haftmann <none@none> |
documentation on code_printing and code_identifier
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
36adb01b |
|
17-Feb-2013 |
haftmann <none@none> |
note on parallel computation
|
| #
ff347444 |
|
07-Oct-2012 |
haftmann <none@none> |
consolidated names of theorems on composition;
generalized former theorem UN_o;
comp_assoc orients to the right, as is more common
|
| #
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
|