| #
a4744357 |
|
19-Jan-2018 |
wenzelm <none@none> |
tuned output of plain name;
|
| #
0bcb05ae |
|
18-Jan-2018 |
wenzelm <none@none> |
clarified access to antiquotation options;
define explicit variants of antiquotations;
output proper Latex.text;
misc tuning and clarification;
|
| #
0ce84d08 |
|
09-Jan-2018 |
wenzelm <none@none> |
clarified modules;
|
| #
ea1397b9 |
|
20-Sep-2017 |
wenzelm <none@none> |
avoid duplicate message for @{action} in particular (see also @{action} within Pure);
|
| #
4d17f0a5 |
|
03-Apr-2016 |
wenzelm <none@none> |
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
|
| #
49773b00 |
|
20-Dec-2015 |
wenzelm <none@none> |
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
|
| #
2b0a18f5 |
|
10-Nov-2015 |
wenzelm <none@none> |
more thorough check_action, including completion;
|
| #
1135bad0 |
|
10-Nov-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
2de3e47b |
|
10-Nov-2015 |
wenzelm <none@none> |
more thorough check_command, including completion;
|
| #
c1388436 |
|
10-Nov-2015 |
wenzelm <none@none> |
clarified modules;
|
| #
2ee63cf1 |
|
10-Nov-2015 |
wenzelm <none@none> |
unused;
|
| #
aa87c472 |
|
10-Nov-2015 |
wenzelm <none@none> |
ignore pointless/unused options;
|
| #
fbdbea19 |
|
17-Oct-2015 |
wenzelm <none@none> |
clarified Latex.environment;
|
| #
f739ffa6 |
|
25-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
8c11536a |
|
22-Dec-2014 |
wenzelm <none@none> |
system option "pretty_margin" is superseded by "thy_output_margin";
|
| #
91c3d5c1 |
|
03-Dec-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
a045e8ed |
|
03-Dec-2014 |
wenzelm <none@none> |
tuned;
|
| #
fb314c8c |
|
30-Nov-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
1c812fe9 |
|
30-Nov-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
9bbace2c |
|
29-Nov-2014 |
wenzelm <none@none> |
more abstract type Input.source;
|
| #
f19e7944 |
|
11-Nov-2014 |
wenzelm <none@none> |
more position information, e.g. relevant for errors in generated ML source;
|
| #
63440213 |
|
07-Nov-2014 |
wenzelm <none@none> |
clarified keyword categories;
tuned;
|
| #
c12ca051 |
|
07-Nov-2014 |
wenzelm <none@none> |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
|
| #
7ecf819b |
|
06-Nov-2014 |
wenzelm <none@none> |
more explicit Keyword.keywords;
|
| #
514ac706 |
|
06-Nov-2014 |
wenzelm <none@none> |
prefer explicit Keyword.keywords;
|
| #
df4ccf3c |
|
05-Nov-2014 |
wenzelm <none@none> |
explicit type Keyword.keywords;
tuned signature;
|
| #
40f4b0f2 |
|
20-Oct-2014 |
wenzelm <none@none> |
official support for "tt" style variants, avoid fragile \verb in LaTeX;
official document antiquotation @{verbatim};
|
| #
a100f9a4 |
|
28-Aug-2014 |
wenzelm <none@none> |
more liberal embedded "text", which includes cartouches;
|
| #
0da05f9f |
|
12-Aug-2014 |
wenzelm <none@none> |
tuned signature according to Scala version -- prefer explicit argument;
|
| #
c2b703ca |
|
01-Jul-2014 |
wenzelm <none@none> |
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
|
| #
cf1618fb |
|
16-Jun-2014 |
wenzelm <none@none> |
formal check of jEdit actions;
--HG--
extra : rebase_source : bb6bf0da15da80fb865331713cf8387c0e9e7999
|
| #
55bc055b |
|
08-Apr-2014 |
wenzelm <none@none> |
more uniform ML/document antiquotations;
|
| #
2ff916cd |
|
27-Mar-2014 |
wenzelm <none@none> |
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
more explicit ML_Compiler.flags;
|
| #
b6e6a472 |
|
26-Mar-2014 |
wenzelm <none@none> |
prefer Context_Position where a context is available;
prefer explicit Context_Position.is_visible -- avoid redundant message composition;
tuned signature;
|
| #
86334bff |
|
25-Mar-2014 |
wenzelm <none@none> |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
| #
bcd9b054 |
|
25-Mar-2014 |
wenzelm <none@none> |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
| #
7216e79c |
|
18-Mar-2014 |
wenzelm <none@none> |
clarifed module name;
--HG--
rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML
rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala
rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala
|
| #
fd286c1c |
|
17-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
70a468bf |
|
13-Mar-2014 |
wenzelm <none@none> |
added ML antiquotation @{path};
|
| #
4b7129c5 |
|
12-Mar-2014 |
wenzelm <none@none> |
ML_Context.check_antiquotation still required;
|
| #
74f7db07 |
|
12-Mar-2014 |
wenzelm <none@none> |
tuned;
|
| #
2bb60506 |
|
12-Mar-2014 |
wenzelm <none@none> |
some document antiquotations for Isabelle/jEdit elements;
modernized theory setup;
|
| #
6a3623e0 |
|
08-Mar-2014 |
wenzelm <none@none> |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
proper context for global data;
tuned signature;
|
| #
8bbe4afd |
|
02-Mar-2014 |
wenzelm <none@none> |
clarified names of antiquotations and markup;
more documentation;
|
| #
2598ec7f |
|
01-Mar-2014 |
wenzelm <none@none> |
more markup for ML source;
|
| #
0e1799d7 |
|
01-Mar-2014 |
wenzelm <none@none> |
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
|
| #
54bcc488 |
|
25-Feb-2014 |
wenzelm <none@none> |
proper context for global data;
|
| #
8573c777 |
|
25-Feb-2014 |
wenzelm <none@none> |
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
removed obsolete Method.Source_i;
proper context for global data;
tuned messages;
|
| #
8e7e6d30 |
|
09-Dec-2013 |
wenzelm <none@none> |
provide @{file_unchecked} in Isabelle/Pure;
|
| #
ad691c1f |
|
07-Nov-2013 |
wenzelm <none@none> |
misc tuning;
|
| #
c1eacf5d |
|
18-Aug-2013 |
wenzelm <none@none> |
more markup;
|
| #
60925a74 |
|
16-Aug-2013 |
wenzelm <none@none> |
check_tool wrt. official ISABELLE_TOOLS;
added Path.split (cf. Scala version);
|
| #
fd79a7ae |
|
16-Aug-2013 |
wenzelm <none@none> |
more markup via Name_Space.check;
tuned signature;
|
| #
77814f5e |
|
15-Jun-2013 |
wenzelm <none@none> |
updated operations on proof terms;
--HG--
extra : rebase_source : 3054c2c4d698768286f9b65b7f62b6d21b79da0c
|
| #
9336ad82 |
|
26-Nov-2012 |
wenzelm <none@none> |
tuned signature;
tuned;
|
| #
95d64a2f |
|
25-Nov-2012 |
wenzelm <none@none> |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
| #
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
|