Thu, 08 May 2008 23:02:23 +0200 replaced some latex macros by antiquotations;
wenzelm [Thu, 08 May 2008 23:02:23 +0200] rev 26860
replaced some latex macros by antiquotations;
Thu, 08 May 2008 22:49:05 +0200 removed obsolete macros;
wenzelm [Thu, 08 May 2008 22:49:05 +0200] rev 26859
removed obsolete macros; tuned;
Thu, 08 May 2008 22:48:33 +0200 removed obsolete math macros;
wenzelm [Thu, 08 May 2008 22:48:33 +0200] rev 26858
removed obsolete math macros;
Thu, 08 May 2008 22:48:09 +0200 depend on style.sty;
wenzelm [Thu, 08 May 2008 22:48:09 +0200] rev 26857
depend on style.sty;
Thu, 08 May 2008 22:32:35 +0200 updated generated file;
wenzelm [Thu, 08 May 2008 22:32:35 +0200] rev 26856
updated generated file;
Thu, 08 May 2008 22:31:23 +0200 depend on ../../antiquote_setup.ML;
wenzelm [Thu, 08 May 2008 22:31:23 +0200] rev 26855
depend on ../../antiquote_setup.ML;
Thu, 08 May 2008 22:20:33 +0200 improved treatment of "_" thanks to underscore.sty;
wenzelm [Thu, 08 May 2008 22:20:33 +0200] rev 26854
improved treatment of "_" thanks to underscore.sty;
Thu, 08 May 2008 22:17:37 +0200 clean_string: map "_" to "\\_" (best used with underscore.sty);
wenzelm [Thu, 08 May 2008 22:17:37 +0200] rev 26853
clean_string: map "_" to "\\_" (best used with underscore.sty);
Thu, 08 May 2008 22:05:15 +0200 misc tuning;
wenzelm [Thu, 08 May 2008 22:05:15 +0200] rev 26852
misc tuning;
Thu, 08 May 2008 14:52:07 +0200 slight tuning of the 1st paragraph
urbanc [Thu, 08 May 2008 14:52:07 +0200] rev 26851
slight tuning of the 1st paragraph
Thu, 08 May 2008 12:31:30 +0200 unused;
wenzelm [Thu, 08 May 2008 12:31:30 +0200] rev 26850
unused;
Thu, 08 May 2008 12:29:18 +0200 converted HOL specific elements;
wenzelm [Thu, 08 May 2008 12:29:18 +0200] rev 26849
converted HOL specific elements;
Thu, 08 May 2008 12:27:19 +0200 added rail setup for verblbrace, verbrbrace;
wenzelm [Thu, 08 May 2008 12:27:19 +0200] rev 26848
added rail setup for verblbrace, verbrbrace;
Thu, 08 May 2008 04:20:08 +0200 added at_set_avoiding lemmas
urbanc [Thu, 08 May 2008 04:20:08 +0200] rev 26847
added at_set_avoiding lemmas
Wed, 07 May 2008 15:32:31 +0200 removed obsolete conversion guide -- converted only section on tactics;
wenzelm [Wed, 07 May 2008 15:32:31 +0200] rev 26846
removed obsolete conversion guide -- converted only section on tactics;
Wed, 07 May 2008 13:38:15 +0200 converted ZF specific elements;
wenzelm [Wed, 07 May 2008 13:38:15 +0200] rev 26845
converted ZF specific elements;
Wed, 07 May 2008 13:05:46 +0200 enabled ThyOutput.source option by default;
wenzelm [Wed, 07 May 2008 13:05:46 +0200] rev 26844
enabled ThyOutput.source option by default;
Wed, 07 May 2008 13:05:13 +0200 output_entity: ignore ThyOutput.source option;
wenzelm [Wed, 07 May 2008 13:05:13 +0200] rev 26843
output_entity: ignore ThyOutput.source option;
Wed, 07 May 2008 13:04:12 +0200 updated generated file;
wenzelm [Wed, 07 May 2008 13:04:12 +0200] rev 26842
updated generated file;
Wed, 07 May 2008 12:56:11 +0200 converted HOLCF specific elements;
wenzelm [Wed, 07 May 2008 12:56:11 +0200] rev 26841
converted HOLCF specific elements;
Wed, 07 May 2008 12:38:55 +0200 added logic-specific sessions;
wenzelm [Wed, 07 May 2008 12:38:55 +0200] rev 26840
added logic-specific sessions;
Wed, 07 May 2008 10:59:54 +0200 Updated.
berghofe [Wed, 07 May 2008 10:59:54 +0200] rev 26839
Updated.
Wed, 07 May 2008 10:59:53 +0200 Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma
berghofe [Wed, 07 May 2008 10:59:53 +0200] rev 26838
Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.
Wed, 07 May 2008 10:59:52 +0200 Replaced instance declarations for sets by instance declarations for bool.
berghofe [Wed, 07 May 2008 10:59:52 +0200] rev 26837
Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.
Wed, 07 May 2008 10:59:51 +0200 Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm,
berghofe [Wed, 07 May 2008 10:59:51 +0200] rev 26836
Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).
Wed, 07 May 2008 10:59:50 +0200 Lookup and union operations on terms are now modulo eta conversion.
berghofe [Wed, 07 May 2008 10:59:50 +0200] rev 26835
Lookup and union operations on terms are now modulo eta conversion.
Wed, 07 May 2008 10:59:49 +0200 Terms returned by decomp are now eta-contracted.
berghofe [Wed, 07 May 2008 10:59:49 +0200] rev 26834
Terms returned by decomp are now eta-contracted.
Wed, 07 May 2008 10:59:48 +0200 Added function for computing instantiation for the subst rule, which is used
berghofe [Wed, 07 May 2008 10:59:48 +0200] rev 26833
Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.
Wed, 07 May 2008 10:59:47 +0200 eq_assumption now uses aeconv instead of aconv.
berghofe [Wed, 07 May 2008 10:59:47 +0200] rev 26832
eq_assumption now uses aeconv instead of aconv.
Wed, 07 May 2008 10:59:46 +0200 - Removed function eta_contract_atom, which did not quite work
berghofe [Wed, 07 May 2008 10:59:46 +0200] rev 26831
- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv
Wed, 07 May 2008 10:59:45 +0200 Replaced Pattern.eta_contract_atom by Envir.eta_contract.
berghofe [Wed, 07 May 2008 10:59:45 +0200] rev 26830
Replaced Pattern.eta_contract_atom by Envir.eta_contract.
Wed, 07 May 2008 10:59:44 +0200 Removed instantiation for set.
berghofe [Wed, 07 May 2008 10:59:44 +0200] rev 26829
Removed instantiation for set.
Wed, 07 May 2008 10:59:43 +0200 Explicitely applied ext in proof of tnd.
berghofe [Wed, 07 May 2008 10:59:43 +0200] rev 26828
Explicitely applied ext in proof of tnd.
Wed, 07 May 2008 10:59:42 +0200 Deleted subset_antisym in a few proofs, because it is
berghofe [Wed, 07 May 2008 10:59:42 +0200] rev 26827
Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.
Wed, 07 May 2008 10:59:41 +0200 - Tuned imports
berghofe [Wed, 07 May 2008 10:59:41 +0200] rev 26826
- Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.
Wed, 07 May 2008 10:59:40 +0200 Manually applied subset_antisym in proof of Compl_fixedpoint, because it is
berghofe [Wed, 07 May 2008 10:59:40 +0200] rev 26825
Manually applied subset_antisym in proof of Compl_fixedpoint, because it is accidentally applied to predicates as well.
Wed, 07 May 2008 10:59:39 +0200 Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped
berghofe [Wed, 07 May 2008 10:59:39 +0200] rev 26824
Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.
Wed, 07 May 2008 10:59:38 +0200 Functions get_branching_types and get_arities now use fold instead of foldl/r.
berghofe [Wed, 07 May 2008 10:59:38 +0200] rev 26823
Functions get_branching_types and get_arities now use fold instead of foldl/r.
Wed, 07 May 2008 10:59:37 +0200 Temporarily disabled invocations of new code generator that do no
berghofe [Wed, 07 May 2008 10:59:37 +0200] rev 26822
Temporarily disabled invocations of new code generator that do no longer work due to the encoding of sets as predicates
Wed, 07 May 2008 10:59:36 +0200 Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"
berghofe [Wed, 07 May 2008 10:59:36 +0200] rev 26821
Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"
Wed, 07 May 2008 10:59:35 +0200 - Deleted arity proofs for set
berghofe [Wed, 07 May 2008 10:59:35 +0200] rev 26820
- Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq
Wed, 07 May 2008 10:59:34 +0200 Replaced union_empty2 by Un_empty_right.
berghofe [Wed, 07 May 2008 10:59:34 +0200] rev 26819
Replaced union_empty2 by Un_empty_right.
Wed, 07 May 2008 10:59:33 +0200 Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
berghofe [Wed, 07 May 2008 10:59:33 +0200] rev 26818
Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that it gets applied to sets as well.
Wed, 07 May 2008 10:59:32 +0200 Deleted instance "set :: ({heap, finite}) heap"
berghofe [Wed, 07 May 2008 10:59:32 +0200] rev 26817
Deleted instance "set :: ({heap, finite}) heap"
Wed, 07 May 2008 10:59:29 +0200 - Declared subset_eq as code lemma
berghofe [Wed, 07 May 2008 10:59:29 +0200] rev 26816
- Declared subset_eq as code lemma - Deleted types_code declaration for sets
Wed, 07 May 2008 10:59:27 +0200 Deleted instantiation "set :: (enum) enum"
berghofe [Wed, 07 May 2008 10:59:27 +0200] rev 26815
Deleted instantiation "set :: (enum) enum"
Wed, 07 May 2008 10:59:24 +0200 Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe [Wed, 07 May 2008 10:59:24 +0200] rev 26814
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with definitions of + and * on functions.
Wed, 07 May 2008 10:59:23 +0200 Rephrased calculational proofs to avoid problems with HO unification
berghofe [Wed, 07 May 2008 10:59:23 +0200] rev 26813
Rephrased calculational proofs to avoid problems with HO unification
Wed, 07 May 2008 10:59:22 +0200 Rephrased forward proofs to avoid problems with HO unification
berghofe [Wed, 07 May 2008 10:59:22 +0200] rev 26812
Rephrased forward proofs to avoid problems with HO unification
Wed, 07 May 2008 10:59:21 +0200 Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification
berghofe [Wed, 07 May 2008 10:59:21 +0200] rev 26811
Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification
Wed, 07 May 2008 10:59:20 +0200 Locally deleted some definitions that were applied too eagerly because
berghofe [Wed, 07 May 2008 10:59:20 +0200] rev 26810
Locally deleted some definitions that were applied too eagerly because of eta-expansion
Wed, 07 May 2008 10:59:19 +0200 - Instantiated parts_insert_substD to avoid problems with HO unification
berghofe [Wed, 07 May 2008 10:59:19 +0200] rev 26809
- Instantiated parts_insert_substD to avoid problems with HO unification - Replaced auto by fastsimp in proof of parts_invKey, since auto looped because of the new encoding of sets
Wed, 07 May 2008 10:59:18 +0200 Instantiated parts_insert_substD to avoid problems with HO unification
berghofe [Wed, 07 May 2008 10:59:18 +0200] rev 26808
Instantiated parts_insert_substD to avoid problems with HO unification
Wed, 07 May 2008 10:59:02 +0200 Replaced blast by fast in proof of parts_singleton, since blast looped
berghofe [Wed, 07 May 2008 10:59:02 +0200] rev 26807
Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.
Wed, 07 May 2008 10:57:19 +0200 Adapted to encoding of sets as predicates
berghofe [Wed, 07 May 2008 10:57:19 +0200] rev 26806
Adapted to encoding of sets as predicates
Wed, 07 May 2008 10:56:58 +0200 Replaced forward proofs of existential statements by backward proofs
berghofe [Wed, 07 May 2008 10:56:58 +0200] rev 26805
Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification
Wed, 07 May 2008 10:56:55 +0200 Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
berghofe [Wed, 07 May 2008 10:56:55 +0200] rev 26804
Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
Wed, 07 May 2008 10:56:52 +0200 - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe [Wed, 07 May 2008 10:56:52 +0200] rev 26803
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set and to_pred attributes, because it is no longer applied automatically - Manually applied predicate1I in proof of accp_subset, because it is no longer part of the claset - Replaced psubset_def by less_le
Wed, 07 May 2008 10:56:50 +0200 Deleted instantiation "set :: (type) itself".
berghofe [Wed, 07 May 2008 10:56:50 +0200] rev 26802
Deleted instantiation "set :: (type) itself".
Wed, 07 May 2008 10:56:49 +0200 - Function dec in Trancl_Tac must eta-contract relation before calling
berghofe [Wed, 07 May 2008 10:56:49 +0200] rev 26801
- Function dec in Trancl_Tac must eta-contract relation before calling decr, since it is now a function and could therefore be in eta-expanded form - The trancl prover now does more eta-contraction itself, so eta-contraction is no longer necessary in Tranclp_tac.
Wed, 07 May 2008 10:56:43 +0200 - Now uses Orderings as parent theory
berghofe [Wed, 07 May 2008 10:56:43 +0200] rev 26800
- Now uses Orderings as parent theory - "'a set" is now just a type abbreviation for "'a => bool" - The instantiation "set :: (type) ord" and the definition of (p)subset is no longer needed, since it is subsumed by the order on functions and booleans. The derived theorems (p)subset_eq can be used as a replacement. - mem_Collect_eq and Collect_mem_eq can now be derived from the definitions of mem and Collect. - Replaced the instantiation "set :: (type) minus" by the two instantiations "fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq can be used as a replacement for the definition set_diff_def - Replaced the instantiation "set :: (type) uminus" by the two instantiations "fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq can be used as a replacement for the definition Compl_def. - Variable P in rule split_if must be instantiated manually in proof of split_if_mem2 due to problems with HO unification - Moved definition of dense linear orders and proofs about LEAST from Orderings to Set - Deleted code setup for sets
Wed, 07 May 2008 10:56:41 +0200 Deleted instance "set :: (type) power" and moved instance
berghofe [Wed, 07 May 2008 10:56:41 +0200] rev 26799
Deleted instance "set :: (type) power" and moved instance "fun :: (type, type) power" to the beginning of the theory
Wed, 07 May 2008 10:56:40 +0200 split_beta is now declared as monotonicity rule, to allow bounded
berghofe [Wed, 07 May 2008 10:56:40 +0200] rev 26798
split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.
Wed, 07 May 2008 10:56:39 +0200 - Added mem_def and predicate1I in some of the proofs
berghofe [Wed, 07 May 2008 10:56:39 +0200] rev 26797
- Added mem_def and predicate1I in some of the proofs - pred_equals_eq and pred_subset_eq are no longer used in the conversion between sets and predicates, because sets and predicates can no longer be distinguished
Wed, 07 May 2008 10:56:38 +0200 - Now imports Code_Setup, rather than Set and Fun, since the theorems
berghofe [Wed, 07 May 2008 10:56:38 +0200] rev 26796
- Now imports Code_Setup, rather than Set and Fun, since the theorems about orderings are already needed in Set - Moved "Dense orders" section to Set, since it requires set notation. - The "Order on sets" section is no longer necessary, since it is subsumed by the order on functions and booleans. - Moved proofs of Least_mono and Least_equality to Set, since they require set notation. - In proof of "instance fun :: (type, order) order", use ext instead of expand_fun_eq, since the latter is not yet available. - predicate1I is no longer declared as introduction rule, since it interferes with subsetI
Wed, 07 May 2008 10:56:37 +0200 - Explicitely applied predicate1I in a few proofs, because it is no longer
berghofe [Wed, 07 May 2008 10:56:37 +0200] rev 26795
- Explicitely applied predicate1I in a few proofs, because it is no longer part of the claset - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set attribute, because it is no longer applied automatically
Wed, 07 May 2008 10:56:36 +0200 - Now imports Fun rather than Orderings
berghofe [Wed, 07 May 2008 10:56:36 +0200] rev 26794
- Now imports Fun rather than Orderings - Moved "Set as lattice" section behind "Fun as lattice" section, since sets are just functions. - The instantiations instantiation set :: (type) distrib_lattice instantiation set :: (type) complete_lattice are no longer needed, and the former definitions inf_set_eq, sup_set_eq, Inf_set_def, and Sup_set_def can now be derived from abstract properties of sup, inf, etc.
Wed, 07 May 2008 10:56:35 +0200 Instantiated some rules to avoid problems with HO unification.
berghofe [Wed, 07 May 2008 10:56:35 +0200] rev 26793
Instantiated some rules to avoid problems with HO unification.
Wed, 07 May 2008 10:56:34 +0200 - Deleted code setup for finite and card
berghofe [Wed, 07 May 2008 10:56:34 +0200] rev 26792
- Deleted code setup for finite and card - Deleted proof of "instance set :: (finite) finite" and modified proof of "instance fun :: (finite, finite) finite", which now uses some ideas from the instance proof for sets - Instantiated arg_cong rule to avoid problems with HO unification
Wed, 07 May 2008 10:56:33 +0200 Instantiated subst rule to avoid problems with HO unification.
berghofe [Wed, 07 May 2008 10:56:33 +0200] rev 26791
Instantiated subst rule to avoid problems with HO unification.
Tue, 06 May 2008 23:33:05 +0200 converted "General logic setup";
wenzelm [Tue, 06 May 2008 23:33:05 +0200] rev 26790
converted "General logic setup";
Tue, 06 May 2008 00:13:01 +0200 misc fixes and tuning;
wenzelm [Tue, 06 May 2008 00:13:01 +0200] rev 26789
misc fixes and tuning;
Tue, 06 May 2008 00:12:03 +0200 updated generated file;
wenzelm [Tue, 06 May 2008 00:12:03 +0200] rev 26788
updated generated file;
Tue, 06 May 2008 00:10:59 +0200 proper scoping of railaliases;
wenzelm [Tue, 06 May 2008 00:10:59 +0200] rev 26787
proper scoping of railaliases;
Tue, 06 May 2008 00:10:23 +0200 moved some railaliases here -- for proper scoping;
wenzelm [Tue, 06 May 2008 00:10:23 +0200] rev 26786
moved some railaliases here -- for proper scoping;
Tue, 06 May 2008 00:08:52 +0200 element: isakeyword markup;
wenzelm [Tue, 06 May 2008 00:08:52 +0200] rev 26785
element: isakeyword markup;
Mon, 05 May 2008 15:27:13 +0200 removed isasymIN -- already defined in isar.sty;
wenzelm [Mon, 05 May 2008 15:27:13 +0200] rev 26784
removed isasymIN -- already defined in isar.sty;
Mon, 05 May 2008 15:23:59 +0200 added isasymIN/STRUCTURE;
wenzelm [Mon, 05 May 2008 15:23:59 +0200] rev 26783
added isasymIN/STRUCTURE;
Mon, 05 May 2008 15:23:21 +0200 converted generic.tex to Thy/Generic.thy;
wenzelm [Mon, 05 May 2008 15:23:21 +0200] rev 26782
converted generic.tex to Thy/Generic.thy;
Sun, 04 May 2008 21:34:44 +0200 removed isasymIMPORTS/BEGIN -- already defined in isar.sty;
wenzelm [Sun, 04 May 2008 21:34:44 +0200] rev 26781
removed isasymIMPORTS/BEGIN -- already defined in isar.sty;
Sat, 03 May 2008 13:36:11 +0200 tuned syntax: props and facts;
wenzelm [Sat, 03 May 2008 13:36:11 +0200] rev 26780
tuned syntax: props and facts;
Sat, 03 May 2008 13:26:08 +0200 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm [Sat, 03 May 2008 13:26:08 +0200] rev 26779
converted refcard.tex to Thy/Quick_Reference.thy;
Sat, 03 May 2008 13:25:27 +0200 added \isasymdash;
wenzelm [Sat, 03 May 2008 13:25:27 +0200] rev 26778
added \isasymdash;
Fri, 02 May 2008 22:49:53 +0200 misc tuning;
wenzelm [Fri, 02 May 2008 22:49:53 +0200] rev 26777
misc tuning;
Fri, 02 May 2008 22:48:51 +0200 updated generated file;
wenzelm [Fri, 02 May 2008 22:48:51 +0200] rev 26776
updated generated file;
Fri, 02 May 2008 22:47:58 +0200 use underscore for underscore;
wenzelm [Fri, 02 May 2008 22:47:58 +0200] rev 26775
use underscore for underscore;
Fri, 02 May 2008 22:47:23 +0200 output_entity: added \mbox{} to prevent hyphenation;
wenzelm [Fri, 02 May 2008 22:47:23 +0200] rev 26774
output_entity: added \mbox{} to prevent hyphenation;
Fri, 02 May 2008 22:43:14 +0200 added more infrastructure for fresh_star
urbanc [Fri, 02 May 2008 22:43:14 +0200] rev 26773
added more infrastructure for fresh_star
Fri, 02 May 2008 18:42:17 +0200 added mising lemma
urbanc [Fri, 02 May 2008 18:42:17 +0200] rev 26772
added mising lemma
Fri, 02 May 2008 18:01:02 +0200 Added documentation
nipkow [Fri, 02 May 2008 18:01:02 +0200] rev 26771
Added documentation
Fri, 02 May 2008 16:39:44 +0200 moved begin and imports to ../isar.sty;
wenzelm [Fri, 02 May 2008 16:39:44 +0200] rev 26770
moved begin and imports to ../isar.sty;
Fri, 02 May 2008 16:38:01 +0200 added begin and imports;
wenzelm [Fri, 02 May 2008 16:38:01 +0200] rev 26769
added begin and imports;
Fri, 02 May 2008 16:36:29 +0200 clean_string: handle { };
wenzelm [Fri, 02 May 2008 16:36:29 +0200] rev 26768
clean_string: handle { };
Fri, 02 May 2008 16:36:05 +0200 converted pure.tex to Thy/pure.thy;
wenzelm [Fri, 02 May 2008 16:36:05 +0200] rev 26767
converted pure.tex to Thy/pure.thy;
Fri, 02 May 2008 16:32:51 +0200 polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc [Fri, 02 May 2008 16:32:51 +0200] rev 26766
polished the proof for atm_prm_fresh and more lemmas for fresh_star
Fri, 02 May 2008 15:49:04 +0200 unfold_locales part of default method.
ballarin [Fri, 02 May 2008 15:49:04 +0200] rev 26765
unfold_locales part of default method.
Fri, 02 May 2008 02:17:07 +0200 extended to be a library of general facts about the lambda calculus
urbanc [Fri, 02 May 2008 02:17:07 +0200] rev 26764
extended to be a library of general facts about the lambda calculus
Fri, 02 May 2008 02:16:10 +0200 tuned some proofs and comments
urbanc [Fri, 02 May 2008 02:16:10 +0200] rev 26763
tuned some proofs and comments
Tue, 29 Apr 2008 19:55:02 +0200 added lemma antiquotation
haftmann [Tue, 29 Apr 2008 19:55:02 +0200] rev 26762
added lemma antiquotation
Tue, 29 Apr 2008 15:25:50 +0200 proper input abbreviations in class
haftmann [Tue, 29 Apr 2008 15:25:50 +0200] rev 26761
proper input abbreviations in class
Tue, 29 Apr 2008 13:41:11 +0200 replaced various macros by antiquotations;
wenzelm [Tue, 29 Apr 2008 13:41:11 +0200] rev 26760
replaced various macros by antiquotations; misc tuning;
Tue, 29 Apr 2008 13:39:54 +0200 more ref macros;
wenzelm [Tue, 29 Apr 2008 13:39:54 +0200] rev 26759
more ref macros;
Tue, 29 Apr 2008 13:39:32 +0200 session based on HOL;
wenzelm [Tue, 29 Apr 2008 13:39:32 +0200] rev 26758
session based on HOL;
Mon, 28 Apr 2008 20:21:11 +0200 thms Max_ge, Min_le: dropped superfluous premise
haftmann [Mon, 28 Apr 2008 20:21:11 +0200] rev 26757
thms Max_ge, Min_le: dropped superfluous premise
Mon, 28 Apr 2008 14:42:13 +0200 proper command/keyword markup;
wenzelm [Mon, 28 Apr 2008 14:42:13 +0200] rev 26756
proper command/keyword markup;
Mon, 28 Apr 2008 14:41:32 +0200 added AND, IS, WHERE symbols;
wenzelm [Mon, 28 Apr 2008 14:41:32 +0200] rev 26755
added AND, IS, WHERE symbols;
Mon, 28 Apr 2008 14:22:42 +0200 converted syntax.tex to Thy/syntax.thy;
wenzelm [Mon, 28 Apr 2008 14:22:42 +0200] rev 26754
converted syntax.tex to Thy/syntax.thy;
Mon, 28 Apr 2008 13:41:04 +0200 dropping return in imperative monad bindings
haftmann [Mon, 28 Apr 2008 13:41:04 +0200] rev 26753
dropping return in imperative monad bindings
Sun, 27 Apr 2008 17:13:01 +0200 corrected ML semantics
haftmann [Sun, 27 Apr 2008 17:13:01 +0200] rev 26752
corrected ML semantics
Sat, 26 Apr 2008 13:20:16 +0200 added setup for Isar entities;
wenzelm [Sat, 26 Apr 2008 13:20:16 +0200] rev 26751
added setup for Isar entities; tuned;
Sat, 26 Apr 2008 08:49:31 +0200 fixed recdef, broken by my previous commit
krauss [Sat, 26 Apr 2008 08:49:31 +0200] rev 26750
fixed recdef, broken by my previous commit
Fri, 25 Apr 2008 16:28:06 +0200 * New attribute "termination_simp": Simp rules for termination proofs
krauss [Fri, 25 Apr 2008 16:28:06 +0200] rev 26749
* New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size
Fri, 25 Apr 2008 15:30:33 +0200 Merged theories about wellfoundedness into one: Wellfounded.thy
krauss [Fri, 25 Apr 2008 15:30:33 +0200] rev 26748
Merged theories about wellfoundedness into one: Wellfounded.thy
Thu, 24 Apr 2008 16:53:04 +0200 moved 'trivial classes' to foundation of code generator
haftmann [Thu, 24 Apr 2008 16:53:04 +0200] rev 26747
moved 'trivial classes' to foundation of code generator
Thu, 24 Apr 2008 11:38:42 +0200 tuned index commands;
wenzelm [Thu, 24 Apr 2008 11:38:42 +0200] rev 26746
tuned index commands;
Thu, 24 Apr 2008 11:38:10 +0200 more abstract index commands;
wenzelm [Thu, 24 Apr 2008 11:38:10 +0200] rev 26745
more abstract index commands;
Thu, 24 Apr 2008 11:05:19 +0200 added \indexoutersyntax;
wenzelm [Thu, 24 Apr 2008 11:05:19 +0200] rev 26744
added \indexoutersyntax; removed permuted index;
Wed, 23 Apr 2008 19:36:18 +0200 fixed proof
haftmann [Wed, 23 Apr 2008 19:36:18 +0200] rev 26743
fixed proof
Wed, 23 Apr 2008 15:04:14 +0200 misc cleanup;
wenzelm [Wed, 23 Apr 2008 15:04:14 +0200] rev 26742
misc cleanup;
Wed, 23 Apr 2008 12:13:08 +0200 converted intro.tex to Thy/intro.thy;
wenzelm [Wed, 23 Apr 2008 12:13:08 +0200] rev 26741
converted intro.tex to Thy/intro.thy;
(0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip