| #
ef845594 |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified signature;
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
| #
03cbd216 |
|
07-Nov-2014 |
wenzelm <none@none> |
eliminated pointless check -- command definitions are subject to theory context;
|
| #
e9ebba3f |
|
16-Aug-2014 |
wenzelm <none@none> |
clarified order of rules;
|
| #
65e9d738 |
|
16-Aug-2014 |
wenzelm <none@none> |
clarified order of rules for match_tac/resolve_tac;
|
| #
db5aeb3c |
|
16-Aug-2014 |
wenzelm <none@none> |
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
|
| #
b32c43f2 |
|
12-May-2014 |
wenzelm <none@none> |
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
|
| #
b7d9f971 |
|
22-Mar-2014 |
wenzelm <none@none> |
avoid hard-wired theory names;
|
| #
d3dc194f |
|
20-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
83bef5f0 |
|
01-Jan-2014 |
wenzelm <none@none> |
clarified simplifier context;
eliminated Simplifier.global_context;
|
| #
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
|
| #
42e9b2b9 |
|
30-Jul-2013 |
wenzelm <none@none> |
type theory is purely value-oriented;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
0fe14a59 |
|
10-Apr-2013 |
wenzelm <none@none> |
more standard module name Axclass (according to file name);
|
| #
951e5a48 |
|
09-Oct-2012 |
huffman <none@none> |
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
removed '(open)', '(set_name)' and '(open set_name)' options
|
| #
150d8520 |
|
16-Mar-2012 |
wenzelm <none@none> |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
| #
de9fb383 |
|
15-Mar-2012 |
wenzelm <none@none> |
prefer formally checked @{keyword} parser;
|
| #
62ec754a |
|
13-Mar-2012 |
wenzelm <none@none> |
more explicit indication of def names;
|
| #
f02a9aca |
|
27-Feb-2012 |
wenzelm <none@none> |
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
|
| #
90b3bab1 |
|
27-Nov-2011 |
wenzelm <none@none> |
more antiquotations;
|
| #
50fe8111 |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned Named_Thms: proper binding;
|
| #
131ea083 |
|
08-Aug-2011 |
huffman <none@none> |
HOLCF: fix warnings about unreferenced identifiers
|
| #
bc193659 |
|
08-Aug-2011 |
huffman <none@none> |
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
|
| #
7dd8cd36 |
|
17-Apr-2011 |
wenzelm <none@none> |
added Binding.print convenience, which includes quote already;
|
| #
13a7cd41 |
|
17-Apr-2011 |
wenzelm <none@none> |
report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
91214357 |
|
29-Mar-2011 |
wenzelm <none@none> |
tuned headers;
|
| #
0b6e7954 |
|
04-Jan-2011 |
huffman <none@none> |
change some lemma names containing 'UU' to 'bottom'
|
| #
0cc893a8 |
|
20-Dec-2010 |
huffman <none@none> |
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
|
| #
d23730c2 |
|
19-Dec-2010 |
huffman <none@none> |
use deflations over type 'udom u' to represent predomains;
removed now-unnecessary class liftdomain;
|
| #
7c56eb3d |
|
19-Dec-2010 |
huffman <none@none> |
type 'defl' takes a type parameter again (cf. b525988432e9)
|
| #
384f4208 |
|
30-Nov-2010 |
huffman <none@none> |
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
|
| #
ac66525c |
|
30-Nov-2010 |
huffman <none@none> |
remove gratuitous semicolons from ML code
|
| #
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
|