#
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
cd839e78 |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified imports;
|
#
9420a93e |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified directory structure; --HG-- rename : src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy => src/HOL/HOLCF/IOA/Abstraction.thy rename : src/HOL/HOLCF/IOA/meta_theory/Asig.thy => src/HOL/HOLCF/IOA/Asig.thy rename : src/HOL/HOLCF/IOA/meta_theory/Automata.thy => src/HOL/HOLCF/IOA/Automata.thy rename : src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy => src/HOL/HOLCF/IOA/CompoExecs.thy rename : src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy => src/HOL/HOLCF/IOA/CompoScheds.thy rename : src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy => src/HOL/HOLCF/IOA/CompoTraces.thy rename : src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy => src/HOL/HOLCF/IOA/Compositionality.thy rename : src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy => src/HOL/HOLCF/IOA/Deadlock.thy rename : src/HOL/HOLCF/IOA/meta_theory/IOA.thy => src/HOL/HOLCF/IOA/IOA.thy rename : src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy => src/HOL/HOLCF/IOA/LiveIOA.thy rename : src/HOL/HOLCF/IOA/meta_theory/Pred.thy => src/HOL/HOLCF/IOA/Pred.thy rename : src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy => src/HOL/HOLCF/IOA/RefCorrectness.thy rename : src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy => src/HOL/HOLCF/IOA/RefMappings.thy rename : src/HOL/HOLCF/IOA/meta_theory/Seq.thy => src/HOL/HOLCF/IOA/Seq.thy rename : src/HOL/HOLCF/IOA/meta_theory/Sequence.thy => src/HOL/HOLCF/IOA/Sequence.thy rename : src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy => src/HOL/HOLCF/IOA/ShortExecutions.thy rename : src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy => src/HOL/HOLCF/IOA/SimCorrectness.thy rename : src/HOL/HOLCF/IOA/meta_theory/Simulations.thy => src/HOL/HOLCF/IOA/Simulations.thy rename : src/HOL/HOLCF/IOA/meta_theory/TL.thy => src/HOL/HOLCF/IOA/TL.thy rename : src/HOL/HOLCF/IOA/meta_theory/TLS.thy => src/HOL/HOLCF/IOA/TLS.thy rename : src/HOL/HOLCF/IOA/meta_theory/Traces.thy => src/HOL/HOLCF/IOA/Traces.thy
|
#
d6002696 |
|
30-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
5d9293a4 |
|
30-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
#
df44ab4c |
|
27-Aug-2015 |
haftmann <none@none> |
standardized some occurences of ancient "split" alias --HG-- extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5
|
#
e5735396 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
7bae4824 |
|
23-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
14ffc3e9 |
|
13-May-2011 |
wenzelm <none@none> |
clarified map_simpset versus Simplifier.map_simpset_global;
|
#
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
|
#
91214357 |
|
29-Mar-2011 |
wenzelm <none@none> |
tuned headers;
|
#
48096e82 |
|
03-Dec-2010 |
wenzelm <none@none> |
recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;
|
#
942babe3 |
|
27-Nov-2010 |
huffman <none@none> |
moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile; --HG-- rename : src/HOLCF/Adm.thy => src/HOL/HOLCF/Adm.thy rename : src/HOLCF/Algebraic.thy => src/HOL/HOLCF/Algebraic.thy rename : src/HOLCF/Bifinite.thy => src/HOL/HOLCF/Bifinite.thy rename : src/HOLCF/Cfun.thy => src/HOL/HOLCF/Cfun.thy rename : src/HOLCF/CompactBasis.thy => src/HOL/HOLCF/CompactBasis.thy rename : src/HOLCF/Completion.thy => src/HOL/HOLCF/Completion.thy rename : src/HOLCF/Cont.thy => src/HOL/HOLCF/Cont.thy rename : src/HOLCF/ConvexPD.thy => src/HOL/HOLCF/ConvexPD.thy rename : src/HOLCF/Cpodef.thy => src/HOL/HOLCF/Cpodef.thy rename : src/HOLCF/Cprod.thy => src/HOL/HOLCF/Cprod.thy rename : src/HOLCF/Deflation.thy => src/HOL/HOLCF/Deflation.thy rename : src/HOLCF/Discrete.thy => src/HOL/HOLCF/Discrete.thy rename : src/HOLCF/Domain.thy => src/HOL/HOLCF/Domain.thy rename : src/HOLCF/Domain_Aux.thy => src/HOL/HOLCF/Domain_Aux.thy rename : src/HOLCF/FOCUS/Buffer.thy => src/HOL/HOLCF/FOCUS/Buffer.thy rename : src/HOLCF/FOCUS/Buffer_adm.thy => src/HOL/HOLCF/FOCUS/Buffer_adm.thy rename : src/HOLCF/FOCUS/FOCUS.thy => src/HOL/HOLCF/FOCUS/FOCUS.thy rename : src/HOLCF/FOCUS/Fstream.thy => src/HOL/HOLCF/FOCUS/Fstream.thy rename : src/HOLCF/FOCUS/Fstreams.thy => src/HOL/HOLCF/FOCUS/Fstreams.thy rename : src/HOLCF/FOCUS/README.html => src/HOL/HOLCF/FOCUS/README.html rename : src/HOLCF/FOCUS/ROOT.ML => src/HOL/HOLCF/FOCUS/ROOT.ML rename : src/HOLCF/FOCUS/Stream_adm.thy => src/HOL/HOLCF/FOCUS/Stream_adm.thy rename : src/HOLCF/Fix.thy => src/HOL/HOLCF/Fix.thy rename : src/HOLCF/Fixrec.thy => src/HOL/HOLCF/Fixrec.thy rename : src/HOLCF/Fun_Cpo.thy => src/HOL/HOLCF/Fun_Cpo.thy rename : src/HOLCF/HOLCF.thy => src/HOL/HOLCF/HOLCF.thy rename : src/HOLCF/IMP/Denotational.thy => src/HOL/HOLCF/IMP/Denotational.thy rename : src/HOLCF/IMP/HoareEx.thy => src/HOL/HOLCF/IMP/HoareEx.thy rename : src/HOLCF/IMP/README.html => src/HOL/HOLCF/IMP/README.html rename : src/HOLCF/IMP/ROOT.ML => src/HOL/HOLCF/IMP/ROOT.ML rename : src/HOLCF/IMP/document/root.bib => src/HOL/HOLCF/IMP/document/root.bib rename : src/HOLCF/IMP/document/root.tex => src/HOL/HOLCF/IMP/document/root.tex rename : src/HOLCF/IOA/ABP/Abschannel.thy => src/HOL/HOLCF/IOA/ABP/Abschannel.thy rename : src/HOLCF/IOA/ABP/Abschannel_finite.thy => src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy rename : src/HOLCF/IOA/ABP/Action.thy => src/HOL/HOLCF/IOA/ABP/Action.thy rename : src/HOLCF/IOA/ABP/Check.ML => src/HOL/HOLCF/IOA/ABP/Check.ML rename : src/HOLCF/IOA/ABP/Correctness.thy => src/HOL/HOLCF/IOA/ABP/Correctness.thy rename : src/HOLCF/IOA/ABP/Env.thy => src/HOL/HOLCF/IOA/ABP/Env.thy rename : src/HOLCF/IOA/ABP/Impl.thy => src/HOL/HOLCF/IOA/ABP/Impl.thy rename : src/HOLCF/IOA/ABP/Impl_finite.thy => src/HOL/HOLCF/IOA/ABP/Impl_finite.thy rename : src/HOLCF/IOA/ABP/Lemmas.thy => src/HOL/HOLCF/IOA/ABP/Lemmas.thy rename : src/HOLCF/IOA/ABP/Packet.thy => src/HOL/HOLCF/IOA/ABP/Packet.thy rename : src/HOLCF/IOA/ABP/ROOT.ML => src/HOL/HOLCF/IOA/ABP/ROOT.ML rename : src/HOLCF/IOA/ABP/Read_me => src/HOL/HOLCF/IOA/ABP/Read_me rename : src/HOLCF/IOA/ABP/Receiver.thy => src/HOL/HOLCF/IOA/ABP/Receiver.thy rename : src/HOLCF/IOA/ABP/Sender.thy => src/HOL/HOLCF/IOA/ABP/Sender.thy rename : src/HOLCF/IOA/ABP/Spec.thy => src/HOL/HOLCF/IOA/ABP/Spec.thy rename : src/HOLCF/IOA/NTP/Abschannel.thy => src/HOL/HOLCF/IOA/NTP/Abschannel.thy rename : src/HOLCF/IOA/NTP/Action.thy => src/HOL/HOLCF/IOA/NTP/Action.thy rename : src/HOLCF/IOA/NTP/Correctness.thy => src/HOL/HOLCF/IOA/NTP/Correctness.thy rename : src/HOLCF/IOA/NTP/Impl.thy => src/HOL/HOLCF/IOA/NTP/Impl.thy rename : src/HOLCF/IOA/NTP/Lemmas.thy => src/HOL/HOLCF/IOA/NTP/Lemmas.thy rename : src/HOLCF/IOA/NTP/Multiset.thy => src/HOL/HOLCF/IOA/NTP/Multiset.thy rename : src/HOLCF/IOA/NTP/Packet.thy => src/HOL/HOLCF/IOA/NTP/Packet.thy rename : src/HOLCF/IOA/NTP/ROOT.ML => src/HOL/HOLCF/IOA/NTP/ROOT.ML rename : src/HOLCF/IOA/NTP/Read_me => src/HOL/HOLCF/IOA/NTP/Read_me rename : src/HOLCF/IOA/NTP/Receiver.thy => src/HOL/HOLCF/IOA/NTP/Receiver.thy rename : src/HOLCF/IOA/NTP/Sender.thy => src/HOL/HOLCF/IOA/NTP/Sender.thy rename : src/HOLCF/IOA/NTP/Spec.thy => src/HOL/HOLCF/IOA/NTP/Spec.thy rename : src/HOLCF/IOA/README.html => src/HOL/HOLCF/IOA/README.html rename : src/HOLCF/IOA/ROOT.ML => src/HOL/HOLCF/IOA/ROOT.ML rename : src/HOLCF/IOA/Storage/Action.thy => src/HOL/HOLCF/IOA/Storage/Action.thy rename : src/HOLCF/IOA/Storage/Correctness.thy => src/HOL/HOLCF/IOA/Storage/Correctness.thy rename : src/HOLCF/IOA/Storage/Impl.thy => src/HOL/HOLCF/IOA/Storage/Impl.thy rename : src/HOLCF/IOA/Storage/ROOT.ML => src/HOL/HOLCF/IOA/Storage/ROOT.ML rename : src/HOLCF/IOA/Storage/Spec.thy => src/HOL/HOLCF/IOA/Storage/Spec.thy rename : src/HOLCF/IOA/ex/ROOT.ML => src/HOL/HOLCF/IOA/ex/ROOT.ML rename : src/HOLCF/IOA/ex/TrivEx.thy => src/HOL/HOLCF/IOA/ex/TrivEx.thy rename : src/HOLCF/IOA/ex/TrivEx2.thy => src/HOL/HOLCF/IOA/ex/TrivEx2.thy rename : src/HOLCF/IOA/meta_theory/Abstraction.thy => src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy rename : src/HOLCF/IOA/meta_theory/Asig.thy => src/HOL/HOLCF/IOA/meta_theory/Asig.thy rename : src/HOLCF/IOA/meta_theory/Automata.thy => src/HOL/HOLCF/IOA/meta_theory/Automata.thy rename : src/HOLCF/IOA/meta_theory/CompoExecs.thy => src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy rename : src/HOLCF/IOA/meta_theory/CompoScheds.thy => src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy rename : src/HOLCF/IOA/meta_theory/CompoTraces.thy => src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy rename : src/HOLCF/IOA/meta_theory/Compositionality.thy => src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy rename : src/HOLCF/IOA/meta_theory/Deadlock.thy => src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy rename : src/HOLCF/IOA/meta_theory/IOA.thy => src/HOL/HOLCF/IOA/meta_theory/IOA.thy rename : src/HOLCF/IOA/meta_theory/LiveIOA.thy => src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy rename : src/HOLCF/IOA/meta_theory/Pred.thy => src/HOL/HOLCF/IOA/meta_theory/Pred.thy rename : src/HOLCF/IOA/meta_theory/RefCorrectness.thy => src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy rename : src/HOLCF/IOA/meta_theory/RefMappings.thy => src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy rename : src/HOLCF/IOA/meta_theory/Seq.thy => src/HOL/HOLCF/IOA/meta_theory/Seq.thy rename : src/HOLCF/IOA/meta_theory/Sequence.thy => src/HOL/HOLCF/IOA/meta_theory/Sequence.thy rename : src/HOLCF/IOA/meta_theory/ShortExecutions.thy => src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy rename : src/HOLCF/IOA/meta_theory/SimCorrectness.thy => src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy rename : src/HOLCF/IOA/meta_theory/Simulations.thy => src/HOL/HOLCF/IOA/meta_theory/Simulations.thy rename : src/HOLCF/IOA/meta_theory/TL.thy => src/HOL/HOLCF/IOA/meta_theory/TL.thy rename : src/HOLCF/IOA/meta_theory/TLS.thy => src/HOL/HOLCF/IOA/meta_theory/TLS.thy rename : src/HOLCF/IOA/meta_theory/Traces.thy => src/HOL/HOLCF/IOA/meta_theory/Traces.thy rename : src/HOLCF/IsaMakefile => src/HOL/HOLCF/IsaMakefile rename : src/HOLCF/Library/Defl_Bifinite.thy => src/HOL/HOLCF/Library/Defl_Bifinite.thy rename : src/HOLCF/Library/HOLCF_Library.thy => src/HOL/HOLCF/Library/HOLCF_Library.thy rename : src/HOLCF/Library/List_Cpo.thy => src/HOL/HOLCF/Library/List_Cpo.thy rename : src/HOLCF/Library/ROOT.ML => src/HOL/HOLCF/Library/ROOT.ML rename : src/HOLCF/Library/Stream.thy => src/HOL/HOLCF/Library/Stream.thy rename : src/HOLCF/Library/Sum_Cpo.thy => src/HOL/HOLCF/Library/Sum_Cpo.thy rename : src/HOLCF/Lift.thy => src/HOL/HOLCF/Lift.thy rename : src/HOLCF/LowerPD.thy => src/HOL/HOLCF/LowerPD.thy rename : src/HOLCF/Map_Functions.thy => src/HOL/HOLCF/Map_Functions.thy rename : src/HOLCF/One.thy => src/HOL/HOLCF/One.thy rename : src/HOLCF/Pcpo.thy => src/HOL/HOLCF/Pcpo.thy rename : src/HOLCF/Plain_HOLCF.thy => src/HOL/HOLCF/Plain_HOLCF.thy rename : src/HOLCF/Porder.thy => src/HOL/HOLCF/Porder.thy rename : src/HOLCF/Powerdomains.thy => src/HOL/HOLCF/Powerdomains.thy rename : src/HOLCF/Product_Cpo.thy => src/HOL/HOLCF/Product_Cpo.thy rename : src/HOLCF/README.html => src/HOL/HOLCF/README.html rename : src/HOLCF/ROOT.ML => src/HOL/HOLCF/ROOT.ML rename : src/HOLCF/Sfun.thy => src/HOL/HOLCF/Sfun.thy rename : src/HOLCF/Sprod.thy => src/HOL/HOLCF/Sprod.thy rename : src/HOLCF/Ssum.thy => src/HOL/HOLCF/Ssum.thy rename : src/HOLCF/Tools/Domain/domain.ML => src/HOL/HOLCF/Tools/Domain/domain.ML rename : src/HOLCF/Tools/Domain/domain_axioms.ML => src/HOL/HOLCF/Tools/Domain/domain_axioms.ML rename : src/HOLCF/Tools/Domain/domain_constructors.ML => src/HOL/HOLCF/Tools/Domain/domain_constructors.ML rename : src/HOLCF/Tools/Domain/domain_induction.ML => src/HOL/HOLCF/Tools/Domain/domain_induction.ML rename : src/HOLCF/Tools/Domain/domain_isomorphism.ML => src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML rename : src/HOLCF/Tools/Domain/domain_take_proofs.ML => src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML rename : src/HOLCF/Tools/cont_consts.ML => src/HOL/HOLCF/Tools/cont_consts.ML rename : src/HOLCF/Tools/cont_proc.ML => src/HOL/HOLCF/Tools/cont_proc.ML rename : src/HOLCF/Tools/cpodef.ML => src/HOL/HOLCF/Tools/cpodef.ML rename : src/HOLCF/Tools/domaindef.ML => src/HOL/HOLCF/Tools/domaindef.ML rename : src/HOLCF/Tools/fixrec.ML => src/HOL/HOLCF/Tools/fixrec.ML rename : src/HOLCF/Tools/holcf_library.ML => src/HOL/HOLCF/Tools/holcf_library.ML rename : src/HOLCF/Tr.thy => src/HOL/HOLCF/Tr.thy rename : src/HOLCF/Tutorial/Domain_ex.thy => src/HOL/HOLCF/Tutorial/Domain_ex.thy rename : src/HOLCF/Tutorial/Fixrec_ex.thy => src/HOL/HOLCF/Tutorial/Fixrec_ex.thy rename : src/HOLCF/Tutorial/New_Domain.thy => src/HOL/HOLCF/Tutorial/New_Domain.thy rename : src/HOLCF/Tutorial/ROOT.ML => src/HOL/HOLCF/Tutorial/ROOT.ML rename : src/HOLCF/Tutorial/document/root.tex => src/HOL/HOLCF/Tutorial/document/root.tex rename : src/HOLCF/Universal.thy => src/HOL/HOLCF/Universal.thy rename : src/HOLCF/Up.thy => src/HOL/HOLCF/Up.thy rename : src/HOLCF/UpperPD.thy => src/HOL/HOLCF/UpperPD.thy rename : src/HOLCF/document/root.tex => src/HOL/HOLCF/document/root.tex rename : src/HOLCF/ex/Dagstuhl.thy => src/HOL/HOLCF/ex/Dagstuhl.thy rename : src/HOLCF/ex/Dnat.thy => src/HOL/HOLCF/ex/Dnat.thy rename : src/HOLCF/ex/Domain_Proofs.thy => src/HOL/HOLCF/ex/Domain_Proofs.thy rename : src/HOLCF/ex/Fix2.thy => src/HOL/HOLCF/ex/Fix2.thy rename : src/HOLCF/ex/Focus_ex.thy => src/HOL/HOLCF/ex/Focus_ex.thy rename : src/HOLCF/ex/Hoare.thy => src/HOL/HOLCF/ex/Hoare.thy rename : src/HOLCF/ex/Letrec.thy => src/HOL/HOLCF/ex/Letrec.thy rename : src/HOLCF/ex/Loop.thy => src/HOL/HOLCF/ex/Loop.thy rename : src/HOLCF/ex/Pattern_Match.thy => src/HOL/HOLCF/ex/Pattern_Match.thy rename : src/HOLCF/ex/Powerdomain_ex.thy => src/HOL/HOLCF/ex/Powerdomain_ex.thy rename : src/HOLCF/ex/ROOT.ML => src/HOL/HOLCF/ex/ROOT.ML rename : src/HOLCF/ex/hoare.txt => src/HOL/HOLCF/ex/hoare.txt
|