wenzelm [Sat, 28 Jan 2006 17:28:59 +0100] rev 18825
removed unatomize;
added versions of meta_rewrite, unfold, fold;
wenzelm [Sat, 28 Jan 2006 17:28:58 +0100] rev 18824
(un)fold: support object-level rewrites;
wenzelm [Sat, 28 Jan 2006 17:28:57 +0100] rev 18823
added print_consts;
tuned;
wenzelm [Sat, 28 Jan 2006 17:28:56 +0100] rev 18822
removed obsolete keyword 'files';
wenzelm [Sat, 28 Jan 2006 17:28:55 +0100] rev 18821
(un)folded: support object-level rewrites;
wenzelm [Sat, 28 Jan 2006 17:28:54 +0100] rev 18820
added equals_cong;
wenzelm [Sat, 28 Jan 2006 17:28:53 +0100] rev 18819
added Isar/local_defs.ML;
wenzelm [Sat, 28 Jan 2006 17:28:52 +0100] rev 18818
LocalDefs.add_def;
wenzelm [Sat, 28 Jan 2006 17:28:51 +0100] rev 18817
LocalDefs.def_export;
wenzelm [Sat, 28 Jan 2006 17:28:50 +0100] rev 18816
tuned proofs;
wenzelm [Sat, 28 Jan 2006 17:28:48 +0100] rev 18815
Pure/Isar: (un)folded, (un)fold, unfolding support
object-level rewrite rules;
ML/Isar: installed ML toplevel pretty printer for type Proof.context;
webertj [Fri, 27 Jan 2006 20:17:24 +0100] rev 18814
interrupt_timeout for Poly replaced by stub
wenzelm [Fri, 27 Jan 2006 19:05:24 +0100] rev 18813
added atomize_iff;
wenzelm [Fri, 27 Jan 2006 19:03:19 +0100] rev 18812
renamed Pretty.gen_list to Pretty.enum;
wenzelm [Fri, 27 Jan 2006 19:03:17 +0100] rev 18811
swapped theory_context;
wenzelm [Fri, 27 Jan 2006 19:03:16 +0100] rev 18810
swapped Toplevel.theory_context;
definition(_i): actually rulify as well, support more of object-logic;
definition(_i): more precise treatment of local fixes;
wenzelm [Fri, 27 Jan 2006 19:03:15 +0100] rev 18809
added invent_fixes;
added debug flag, pprint_context;
wenzelm [Fri, 27 Jan 2006 19:03:14 +0100] rev 18808
swapped Toplevel.theory_context;
tuned;
wenzelm [Fri, 27 Jan 2006 19:03:13 +0100] rev 18807
renamed reverse_atomize to unatomize;
added rulify_term/tac;
wenzelm [Fri, 27 Jan 2006 19:03:12 +0100] rev 18806
init: include view;
swapped Toplevel.theory_context;
removed obsolete smart_note_thmss;
moved note_thmss_qualified to PureThy;
unified code of note_thmss(_i), add_thmss, locale_results;
wenzelm [Fri, 27 Jan 2006 19:03:11 +0100] rev 18805
improved 'notes', including proper treatment of locale results;
tuned;
wenzelm [Fri, 27 Jan 2006 19:03:10 +0100] rev 18804
swapped Toplevel.theory_context;
wenzelm [Fri, 27 Jan 2006 19:03:09 +0100] rev 18803
Locale.init;
wenzelm [Fri, 27 Jan 2006 19:03:08 +0100] rev 18802
renamed gen_list to enum;
added separate;
tuned;
wenzelm [Fri, 27 Jan 2006 19:03:07 +0100] rev 18801
moved theorem tags from Drule to PureThy;
replaced kind attribute by kind string;
tuned name_multi: index > 1 only;
added note_thmss_qualified (from Isar/locale.ML);
wenzelm [Fri, 27 Jan 2006 19:03:05 +0100] rev 18800
added ProofContext.pprint_context (depends on ProofContext.debug);
wenzelm [Fri, 27 Jan 2006 19:03:02 +0100] rev 18799
moved theorem tags from Drule to PureThy;
paulson [Fri, 27 Jan 2006 18:29:33 +0100] rev 18798
tidying up SPASS output
paulson [Fri, 27 Jan 2006 18:29:11 +0100] rev 18797
tidying
paulson [Fri, 27 Jan 2006 18:28:55 +0100] rev 18796
better reporting
ballarin [Fri, 27 Jan 2006 16:05:23 +0100] rev 18795
Interface to access the specification of a named locale.
mengj [Fri, 27 Jan 2006 05:46:39 +0100] rev 18794
Added new file Tools/ATP/reduce_axiomsN.ML
mengj [Fri, 27 Jan 2006 05:45:25 +0100] rev 18793
Added in new file Tools/ATP/reduce_axiomsN.ML
mengj [Fri, 27 Jan 2006 05:37:12 +0100] rev 18792
Changed codes that call relevance filter.
mengj [Fri, 27 Jan 2006 05:34:20 +0100] rev 18791
Relevance filtering. Has replaced the previous version.
webertj [Thu, 26 Jan 2006 20:42:15 +0100] rev 18790
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
webertj [Thu, 26 Jan 2006 20:17:54 +0100] rev 18789
smaller example to prevent timeout
berghofe [Thu, 26 Jan 2006 17:58:01 +0100] rev 18788
Fixed bug in code generator for primitive definitions that
caused dependencies to get mixed up.
berghofe [Thu, 26 Jan 2006 15:37:14 +0100] rev 18787
Inductive sets with no introduction rules are now allowed as well.
wenzelm [Wed, 25 Jan 2006 00:21:44 +0100] rev 18786
added definition(_i);
wenzelm [Wed, 25 Jan 2006 00:21:43 +0100] rev 18785
renamed export to export_standard (again!), because it includes Drule.local_standard';
added abs_def (from locale.ML);
wenzelm [Wed, 25 Jan 2006 00:21:42 +0100] rev 18784
ProofContext.export_standard;
wenzelm [Wed, 25 Jan 2006 00:21:41 +0100] rev 18783
tuned atomize_cterm;
added reverse_atomize_term/tac;
wenzelm [Wed, 25 Jan 2006 00:21:40 +0100] rev 18782
turned abstract_term into ProofContext.abs_def;
ProofContext.export_standard;
wenzelm [Wed, 25 Jan 2006 00:21:39 +0100] rev 18781
added constant definition;
tuned interfaces;
tuned;
wenzelm [Wed, 25 Jan 2006 00:21:38 +0100] rev 18780
added 'definition';
'spezification': optional fixes;
wenzelm [Wed, 25 Jan 2006 00:21:37 +0100] rev 18779
tuned comment;
wenzelm [Wed, 25 Jan 2006 00:21:36 +0100] rev 18778
export name_multi;
wenzelm [Wed, 25 Jan 2006 00:21:35 +0100] rev 18777
abs_def: improved error;
wenzelm [Wed, 25 Jan 2006 00:21:34 +0100] rev 18776
ObjectLogic.atomize_cterm;
wenzelm [Wed, 25 Jan 2006 00:21:32 +0100] rev 18775
updated;
webertj [Tue, 24 Jan 2006 15:16:06 +0100] rev 18774
works with DPLL solver now
urbanc [Tue, 24 Jan 2006 13:28:06 +0100] rev 18773
the additional freshness-condition in the one-induction
is not needed anywhere.
wenzelm [Tue, 24 Jan 2006 00:44:39 +0100] rev 18772
fixed code_generate syntax;
wenzelm [Tue, 24 Jan 2006 00:43:34 +0100] rev 18771
renamed axiomatize(_i) to axiomatization(_i);
LocalTheory;
wenzelm [Tue, 24 Jan 2006 00:43:33 +0100] rev 18770
renamed inferred_type to inferred_param;
added inferred_fixes;
wenzelm [Tue, 24 Jan 2006 00:43:32 +0100] rev 18769
ProofContext.inferred_param;
wenzelm [Tue, 24 Jan 2006 00:43:31 +0100] rev 18768
removed the_params;
wenzelm [Tue, 24 Jan 2006 00:43:29 +0100] rev 18767
added actual operations;
wenzelm [Tue, 24 Jan 2006 00:43:28 +0100] rev 18766
axiomatization: optional vars;
wenzelm [Tue, 24 Jan 2006 00:43:27 +0100] rev 18765
LocalTheory.pretty_consts;
wenzelm [Tue, 24 Jan 2006 00:43:25 +0100] rev 18764
tuned;
wenzelm [Tue, 24 Jan 2006 00:43:24 +0100] rev 18763
add_finals: prep_consts, i.e. varify type;
wenzelm [Tue, 24 Jan 2006 00:43:23 +0100] rev 18762
added dest_all;
webertj [Mon, 23 Jan 2006 18:20:48 +0100] rev 18761
TimeLimit replaced by interrupt_timeout
webertj [Mon, 23 Jan 2006 17:29:52 +0100] rev 18760
TimeLimit replaced by interrupt_timeout
krauss [Mon, 23 Jan 2006 15:23:31 +0100] rev 18759
Updated to Isabelle 2006-01-23
urbanc [Mon, 23 Jan 2006 15:14:06 +0100] rev 18758
made change for ex1
haftmann [Mon, 23 Jan 2006 14:07:52 +0100] rev 18757
removed problematic keyword 'atom'
haftmann [Mon, 23 Jan 2006 14:06:40 +0100] rev 18756
more general serializer
haftmann [Mon, 23 Jan 2006 14:06:28 +0100] rev 18755
slight steps forward
haftmann [Mon, 23 Jan 2006 14:06:11 +0100] rev 18754
exported after_qed for axclass instance
paulson [Mon, 23 Jan 2006 11:41:54 +0100] rev 18753
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
paulson [Mon, 23 Jan 2006 11:38:43 +0100] rev 18752
Clausification now handles some IFs in rewrite rules (if-split did not work)
paulson [Mon, 23 Jan 2006 11:37:53 +0100] rev 18751
bugfix: induct_tac no longer raises THM "dest_state"
paulson [Mon, 23 Jan 2006 11:36:50 +0100] rev 18750
fixed the <<= notation
paulson [Mon, 23 Jan 2006 11:36:05 +0100] rev 18749
replacement of bool by a datatype (making problems first-order). More lemma names
mengj [Mon, 23 Jan 2006 10:34:38 +0100] rev 18748
Fixed a bug.
urbanc [Sun, 22 Jan 2006 22:16:34 +0100] rev 18747
no essential changes
urbanc [Sun, 22 Jan 2006 22:11:50 +0100] rev 18746
made the change for setup-functions not returning functions
anymore
urbanc [Sun, 22 Jan 2006 21:58:43 +0100] rev 18745
a fixme comments about abs_fun_if, which should be called perm_if
and moved to the "bool"-section
wenzelm [Sun, 22 Jan 2006 18:46:01 +0100] rev 18744
Local theory operations, with optional target locale.
wenzelm [Sun, 22 Jan 2006 18:46:00 +0100] rev 18743
added restore_body;
wenzelm [Sun, 22 Jan 2006 18:45:59 +0100] rev 18742
added the_params;
wenzelm [Sun, 22 Jan 2006 18:45:58 +0100] rev 18741
tuned order;
wenzelm [Sun, 22 Jan 2006 18:45:57 +0100] rev 18740
added Isar/local_theory.ML;
mengj [Sat, 21 Jan 2006 23:22:40 +0100] rev 18739
Ensure dereference is delayed.
wenzelm [Sat, 21 Jan 2006 23:07:26 +0100] rev 18738
tuned;
wenzelm [Sat, 21 Jan 2006 23:02:30 +0100] rev 18737
* ML: simplified type attribute;
wenzelm [Sat, 21 Jan 2006 23:02:29 +0100] rev 18736
simplified type attribute;
removed obsolete tcset operations -- clean data/attribute/method setup;
wenzelm [Sat, 21 Jan 2006 23:02:28 +0100] rev 18735
removed duplicate type_solver (cf. Tools/typechk.ML);
wenzelm [Sat, 21 Jan 2006 23:02:27 +0100] rev 18734
simplified type attribute;
removed rule/declaration (cf. thm.ML);
removed obsolete theory/proof/generic/common;
removed obsolete global/local/context_attribute(_i);
added attribute(_i);
renamed attribute to internal;
wenzelm [Sat, 21 Jan 2006 23:02:25 +0100] rev 18733
simplified type attribute;
added rule/declaration_attribute (from drule.ML);
added theory/proof_attributes;
removed apply(s)_attributes;
wenzelm [Sat, 21 Jan 2006 23:02:24 +0100] rev 18732
simplified type attribute;
moved rule/declaration_attribute to thm.ML;
wenzelm [Sat, 21 Jan 2006 23:02:23 +0100] rev 18731
rename map_theory/proof to theory/proof_map;
added separate map_theory/proof;
wenzelm [Sat, 21 Jan 2006 23:02:21 +0100] rev 18730
tuned proofs;
wenzelm [Sat, 21 Jan 2006 23:02:20 +0100] rev 18729
simplified type attribute;
tuned;
wenzelm [Sat, 21 Jan 2006 23:02:14 +0100] rev 18728
simplified type attribute;
mengj [Fri, 20 Jan 2006 04:53:59 +0100] rev 18727
type information is now also printed.
mengj [Fri, 20 Jan 2006 04:50:01 +0100] rev 18726
added some debugging code.
mengj [Fri, 20 Jan 2006 04:35:23 +0100] rev 18725
fixed a bug
wenzelm [Thu, 19 Jan 2006 21:22:30 +0100] rev 18724
quote "atom";
wenzelm [Thu, 19 Jan 2006 21:22:29 +0100] rev 18723
updated;
wenzelm [Thu, 19 Jan 2006 21:22:27 +0100] rev 18722
* ML/Isar: theory setup has type (theory -> theory);
wenzelm [Thu, 19 Jan 2006 21:22:26 +0100] rev 18721
use/use_thy: Output.toplevel_errors;
wenzelm [Thu, 19 Jan 2006 21:22:25 +0100] rev 18720
added basic syntax;
removed pure syntax;
wenzelm [Thu, 19 Jan 2006 21:22:24 +0100] rev 18719
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
wenzelm [Thu, 19 Jan 2006 21:22:23 +0100] rev 18718
keep: disable Output.toplevel_errors;
program: Output.ML_errors;
wenzelm [Thu, 19 Jan 2006 21:22:22 +0100] rev 18717
run_thy: removed Output.toplevel_errors;
wenzelm [Thu, 19 Jan 2006 21:22:21 +0100] rev 18716
added ML_errors;
wenzelm [Thu, 19 Jan 2006 21:22:20 +0100] rev 18715
use: Output.ML_errors;
wenzelm [Thu, 19 Jan 2006 21:22:19 +0100] rev 18714
Syntax.basic_syn;
wenzelm [Thu, 19 Jan 2006 21:22:18 +0100] rev 18713
setup: theory -> theory;
added syntax (from Syntax/mixfix.ML);
added HTML output syntax for _lambda;
wenzelm [Thu, 19 Jan 2006 21:22:17 +0100] rev 18712
tuned setmp;
wenzelm [Thu, 19 Jan 2006 21:22:16 +0100] rev 18711
setup: theory -> theory;
use_output: Output.ML_errors;
wenzelm [Thu, 19 Jan 2006 21:22:15 +0100] rev 18710
tuned comments;
wenzelm [Thu, 19 Jan 2006 21:22:14 +0100] rev 18709
setup: theory -> theory;
Syntax.appl(C)_syntax;
wenzelm [Thu, 19 Jan 2006 21:22:08 +0100] rev 18708
setup: theory -> theory;
berghofe [Thu, 19 Jan 2006 15:45:10 +0100] rev 18707
Use generic Simplifier.simp_add attribute instead
of Simplifier.simp_add_global.
berghofe [Thu, 19 Jan 2006 14:59:55 +0100] rev 18706
Re-inserted consts_code declaration accidentally deleted
during last commit.