#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
f2d8c31b |
|
26-Dec-2018 |
wenzelm <none@none> |
isabelle update_cartouches -t;
|
#
5589896c |
|
12-Jan-2018 |
wenzelm <none@none> |
isabelle update_cartouches -c;
|
#
a270912e |
|
07-Nov-2014 |
wenzelm <none@none> |
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
|
#
0551f7de |
|
01-Nov-2014 |
wenzelm <none@none> |
eliminated spurious semicolons;
|
#
392cced7 |
|
18-Sep-2014 |
blanchet <none@none> |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again --HG-- rename : src/HOL/Old_Datatype.thy => src/HOL/Library/Old_Datatype.thy
|
#
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
|
#
62659e09 |
|
03-Sep-2013 |
wenzelm <none@none> |
more robust ToyList_Test;
|
#
63332460 |
|
26-Feb-2013 |
wenzelm <none@none> |
updated Toplevel.command_exception;
|
#
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
|