berghofe [Wed, 11 Jul 2007 11:43:31 +0200] rev 23764
New wrapper for defining inductive sets with new inductive
predicate package.
berghofe [Wed, 11 Jul 2007 11:41:30 +0200] rev 23763
Old (co)inductive command is now replaced by (co)inductive_set.
berghofe [Wed, 11 Jul 2007 11:39:59 +0200] rev 23762
Reorganization due to introduction of inductive_set wrapper.
berghofe [Wed, 11 Jul 2007 11:38:25 +0200] rev 23761
Improved code generator for Collect.
berghofe [Wed, 11 Jul 2007 11:36:06 +0200] rev 23760
Renamed inductive2 to inductive.
aspinall [Wed, 11 Jul 2007 11:35:17 +0200] rev 23759
Fix nested PGIP messages. Update for schema simplifications.
berghofe [Wed, 11 Jul 2007 11:34:38 +0200] rev 23758
Moved unify_consts to PrimrecPackage.
berghofe [Wed, 11 Jul 2007 11:32:02 +0200] rev 23757
- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates
berghofe [Wed, 11 Jul 2007 11:29:44 +0200] rev 23756
Adapted to changes in Predicate theory.
berghofe [Wed, 11 Jul 2007 11:28:13 +0200] rev 23755
Adapted to new inductive definition package.
berghofe [Wed, 11 Jul 2007 11:27:46 +0200] rev 23754
Renamed accessible part for predicates to accp.
aspinall [Wed, 11 Jul 2007 11:25:24 +0200] rev 23753
Track schema changes: merge messagecategory with area attributes
berghofe [Wed, 11 Jul 2007 11:25:21 +0200] rev 23752
bot is now a constant.
berghofe [Wed, 11 Jul 2007 11:24:36 +0200] rev 23751
Restored set notation.
berghofe [Wed, 11 Jul 2007 11:23:24 +0200] rev 23750
- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates
aspinall [Wed, 11 Jul 2007 11:22:02 +0200] rev 23749
Track schema changes: remove cleardisplay, proofstate messages. Simplify attributes on cleardisplay, normalresponse.
aspinall [Wed, 11 Jul 2007 11:21:10 +0200] rev 23748
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
berghofe [Wed, 11 Jul 2007 11:16:34 +0200] rev 23747
Renamed inductive2 to inductive.
berghofe [Wed, 11 Jul 2007 11:14:51 +0200] rev 23746
Adapted to new inductive definition package.
berghofe [Wed, 11 Jul 2007 11:13:08 +0200] rev 23745
New operations on tuples with specific arities.
berghofe [Wed, 11 Jul 2007 11:11:39 +0200] rev 23744
Adapted to changes in infrastructure for converting between
sets and predicates.
berghofe [Wed, 11 Jul 2007 11:10:37 +0200] rev 23743
rtrancl and trancl are now defined using inductive_set.
berghofe [Wed, 11 Jul 2007 11:09:15 +0200] rev 23742
Removed wf_implies_wfP and wfP_implies_wf from list of hints again.
berghofe [Wed, 11 Jul 2007 11:07:57 +0200] rev 23741
- Moved infrastructure for converting between sets and predicates
to Tools/inductive_set_package.ML
- Adapted conversion rules to new format (now use standard op :
and Collect operators rather than Collect2 and member(2))
- Removed bounded quantifiers for predicates
berghofe [Wed, 11 Jul 2007 11:04:39 +0200] rev 23740
Adapted to new package for inductive sets.
berghofe [Wed, 11 Jul 2007 11:03:11 +0200] rev 23739
Inserted definition of in_rel again (since member2 was removed).
berghofe [Wed, 11 Jul 2007 11:02:07 +0200] rev 23738
Added ML bindings for sup_fun_eq and sup_bool_eq.
berghofe [Wed, 11 Jul 2007 11:01:24 +0200] rev 23737
top and bot are now constants.
berghofe [Wed, 11 Jul 2007 11:00:46 +0200] rev 23736
Renamed inductive2 to inductive.
berghofe [Wed, 11 Jul 2007 11:00:09 +0200] rev 23735
acc is now defined using inductive_set.
berghofe [Wed, 11 Jul 2007 10:59:23 +0200] rev 23734
Added new package for inductive sets.
berghofe [Wed, 11 Jul 2007 10:53:39 +0200] rev 23733
Adapted to new inductive definition package.
berghofe [Wed, 11 Jul 2007 10:52:20 +0200] rev 23732
Adapted to changes in inductive definition package.
wenzelm [Wed, 11 Jul 2007 00:46:48 +0200] rev 23731
tuned comment markup;
wenzelm [Wed, 11 Jul 2007 00:29:52 +0200] rev 23730
treat OuterLex.Error;
wenzelm [Wed, 11 Jul 2007 00:29:51 +0200] rev 23729
separated Malformed (symbolic char) from Error (bad input);
unparse: Output.escape_malformed;
name_of: use unparse;
wenzelm [Wed, 11 Jul 2007 00:29:50 +0200] rev 23728
Output.escape_malformed;
wenzelm [Wed, 11 Jul 2007 00:29:49 +0200] rev 23727
added escape_malformed (failsafe);
wenzelm [Tue, 10 Jul 2007 23:29:53 +0200] rev 23726
Basic editing of theory sources.
wenzelm [Tue, 10 Jul 2007 23:29:52 +0200] rev 23725
tuned;
wenzelm [Tue, 10 Jul 2007 23:29:51 +0200] rev 23724
export html_mode, begin_document, end_document;
wenzelm [Tue, 10 Jul 2007 23:29:49 +0200] rev 23723
renamed XML.Rawtext to XML.Output;
wenzelm [Tue, 10 Jul 2007 23:29:47 +0200] rev 23722
export get_lexicons;
wenzelm [Tue, 10 Jul 2007 23:29:46 +0200] rev 23721
added kind_of;
unparse: extra care for Malformed;
wenzelm [Tue, 10 Jul 2007 23:29:44 +0200] rev 23720
Markup.enclose;
wenzelm [Tue, 10 Jul 2007 23:29:43 +0200] rev 23719
more markup for inner and outer syntax;
added enclose;
wenzelm [Tue, 10 Jul 2007 23:29:41 +0200] rev 23718
simplified funpow, untabify;
wenzelm [Tue, 10 Jul 2007 23:29:38 +0200] rev 23717
added Thy/thy_edit.ML;
wenzelm [Tue, 10 Jul 2007 23:29:35 +0200] rev 23716
added some markup for outer syntax;
haftmann [Tue, 10 Jul 2007 17:30:57 +0200] rev 23715
clarified merge of module names
haftmann [Tue, 10 Jul 2007 17:30:56 +0200] rev 23714
now a monolithic module
haftmann [Tue, 10 Jul 2007 17:30:54 +0200] rev 23713
now works with SML/NJ
haftmann [Tue, 10 Jul 2007 17:30:53 +0200] rev 23712
tuned
haftmann [Tue, 10 Jul 2007 17:30:52 +0200] rev 23711
improvement for code names
haftmann [Tue, 10 Jul 2007 17:30:51 +0200] rev 23710
removed proof dependency on transitivity theorems
haftmann [Tue, 10 Jul 2007 17:30:50 +0200] rev 23709
moved lfp_induct2 here
haftmann [Tue, 10 Jul 2007 17:30:49 +0200] rev 23708
clarified import
haftmann [Tue, 10 Jul 2007 17:30:47 +0200] rev 23707
moved lfp_induct2 to Relation.thy
haftmann [Tue, 10 Jul 2007 17:30:45 +0200] rev 23706
moved some finite lemmas here
haftmann [Tue, 10 Jul 2007 17:30:43 +0200] rev 23705
moved finite lemmas to Finite_Set.thy
wenzelm [Tue, 10 Jul 2007 16:46:37 +0200] rev 23704
added print_mode setup (from pretty.ML);
removed no_state;
wenzelm [Tue, 10 Jul 2007 16:45:06 +0200] rev 23703
Markup.add_mode;
wenzelm [Tue, 10 Jul 2007 16:45:05 +0200] rev 23702
removed no_state markup -- produce empty state;
Markup.add_mode;
wenzelm [Tue, 10 Jul 2007 16:45:04 +0200] rev 23701
Markup.output;
removed no_state markup -- produce empty state;
wenzelm [Tue, 10 Jul 2007 16:45:03 +0200] rev 23700
moved source cascading from scan.ML to source.ML;
wenzelm [Tue, 10 Jul 2007 16:45:01 +0200] rev 23699
infixr || (more efficient);
tuned signature;
removed unused trace';
moved source cascading from scan.ML to source.ML;
tuned;
wenzelm [Tue, 10 Jul 2007 16:45:00 +0200] rev 23698
moved print_mode setup for markup to markup.ML;
wenzelm [Tue, 10 Jul 2007 16:45:00 +0200] rev 23697
Markup.output;
wenzelm [Tue, 10 Jul 2007 16:44:58 +0200] rev 23696
use position.ML earlier;
aspinall [Tue, 10 Jul 2007 15:45:34 +0200] rev 23695
Add widthN to signature
wenzelm [Tue, 10 Jul 2007 13:12:53 +0200] rev 23694
cd ISABELLE_HOME/etc;
haftmann [Tue, 10 Jul 2007 09:24:43 +0200] rev 23693
adjusted
haftmann [Tue, 10 Jul 2007 09:24:14 +0200] rev 23692
updated keywords
haftmann [Tue, 10 Jul 2007 09:23:17 +0200] rev 23691
simplified, tuned
haftmann [Tue, 10 Jul 2007 09:23:16 +0200] rev 23690
re-expanded paths
haftmann [Tue, 10 Jul 2007 09:23:15 +0200] rev 23689
replaced code generator framework for reflected cooper
haftmann [Tue, 10 Jul 2007 09:23:14 +0200] rev 23688
expanded fragile proof
haftmann [Tue, 10 Jul 2007 09:23:13 +0200] rev 23687
extended - convers now basic lcm properties also
haftmann [Tue, 10 Jul 2007 09:23:12 +0200] rev 23686
constant dvd now in class target
haftmann [Tue, 10 Jul 2007 09:23:11 +0200] rev 23685
moved lemma zdvd_period here
haftmann [Tue, 10 Jul 2007 09:23:10 +0200] rev 23684
introduced (auxiliary) class dvd_mod for more convenient code generation
wenzelm [Tue, 10 Jul 2007 00:43:51 +0200] rev 23683
tuned;
wenzelm [Tue, 10 Jul 2007 00:17:52 +0200] rev 23682
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm [Mon, 09 Jul 2007 23:12:51 +0200] rev 23681
tuned dead code;
wenzelm [Mon, 09 Jul 2007 23:12:49 +0200] rev 23680
use Position.file_of;
removed strange comments;
wenzelm [Mon, 09 Jul 2007 23:12:46 +0200] rev 23679
toplevel_source: interactive flag indicates intermittent error_msg;
nested source: error msg passed to recover;
tuned source positions;
wenzelm [Mon, 09 Jul 2007 23:12:45 +0200] rev 23678
Malformed token: error msg;
scan: explicit handling of malformed symbols from previous stage;
source: interactive flag indicates intermittent error_msg;
tuned;
wenzelm [Mon, 09 Jul 2007 23:12:44 +0200] rev 23677
adapted OuterLex/T.source;
wenzelm [Mon, 09 Jul 2007 23:12:42 +0200] rev 23676
scan: changed treatment of malformed symbols, passed to next stage;
tuned sym_explode;
wenzelm [Mon, 09 Jul 2007 23:12:40 +0200] rev 23675
nested source: error msg passed to recover;
wenzelm [Mon, 09 Jul 2007 23:12:38 +0200] rev 23674
tuned signature;
nested source: error msg passed to recover;
wenzelm [Mon, 09 Jul 2007 23:12:37 +0200] rev 23673
replaced name by file (unquoted);
str_of: markup;
misc cleanup;
wenzelm [Mon, 09 Jul 2007 23:12:36 +0200] rev 23672
moved Path.position to Position.path;
wenzelm [Mon, 09 Jul 2007 23:12:35 +0200] rev 23671
proper position markup;
added properties operation;
tuned;
wenzelm [Mon, 09 Jul 2007 23:12:31 +0200] rev 23670
use position.ML after pretty.ML;
wenzelm [Mon, 09 Jul 2007 23:12:29 +0200] rev 23669
removed target RAW-ProofGeneral (impractical to maintain);
wenzelm [Mon, 09 Jul 2007 22:40:57 +0200] rev 23668
declare: disallow quote (") in names;
wenzelm [Mon, 09 Jul 2007 22:37:48 +0200] rev 23667
removed legacy ML file;
fixed prems_conv;
wenzelm [Mon, 09 Jul 2007 22:06:49 +0200] rev 23666
HOL-Complex-Matrix: fixed deps -- sort of;
obua [Mon, 09 Jul 2007 17:39:55 +0200] rev 23665
adopted to new computing oracle and fixed bugs introduced by tuning
obua [Mon, 09 Jul 2007 17:38:40 +0200] rev 23664
added computing oracle support for HOL and numerals
obua [Mon, 09 Jul 2007 17:36:25 +0200] rev 23663
new version of computing oracle
wenzelm [Mon, 09 Jul 2007 11:44:23 +0200] rev 23662
simplified writeln_fn;
wenzelm [Mon, 09 Jul 2007 11:44:22 +0200] rev 23661
prompt: plain string, not output;
wenzelm [Mon, 09 Jul 2007 11:44:20 +0200] rev 23660
type output = string indicates raw system output;
wenzelm [Sun, 08 Jul 2007 19:52:10 +0200] rev 23659
symbolic output: avoid empty blocks, 1 space for fbreak;
wenzelm [Sun, 08 Jul 2007 19:52:08 +0200] rev 23658
tuned;
wenzelm [Sun, 08 Jul 2007 19:52:05 +0200] rev 23657
thm tag: Markup.property list;
wenzelm [Sun, 08 Jul 2007 19:52:04 +0200] rev 23656
gensym: slightly more obscure prefix descreases probability of name clash;
wenzelm [Sun, 08 Jul 2007 19:51:58 +0200] rev 23655
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm [Sun, 08 Jul 2007 19:51:55 +0200] rev 23654
attribute tagged: single argument;
wenzelm [Sun, 08 Jul 2007 19:51:54 +0200] rev 23653
updated;
wenzelm [Sun, 08 Jul 2007 19:51:52 +0200] rev 23652
simplified Symtab;
wenzelm [Sun, 08 Jul 2007 19:51:51 +0200] rev 23651
renamed ML_exc to ML_exn;
chaieb [Sun, 08 Jul 2007 19:01:32 +0200] rev 23650
Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
chaieb [Sun, 08 Jul 2007 19:01:30 +0200] rev 23649
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb [Sun, 08 Jul 2007 19:01:28 +0200] rev 23648
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb [Sun, 08 Jul 2007 19:01:26 +0200] rev 23647
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
wenzelm [Sun, 08 Jul 2007 13:10:57 +0200] rev 23646
simplified/more robust print_state;
more robust prompt markup;
wenzelm [Sun, 08 Jul 2007 13:10:54 +0200] rev 23645
export mode_markup;
added symbolic output (via print_mode);
misc cleanup;
wenzelm [Sun, 08 Jul 2007 13:10:51 +0200] rev 23644
added markup for pretty printing;
chaieb [Sun, 08 Jul 2007 12:20:56 +0200] rev 23643
Corrected erronus use of compiletime context to the runtime context
wenzelm [Sat, 07 Jul 2007 18:47:47 +0200] rev 23642
make smlnj happy;
wenzelm [Sat, 07 Jul 2007 18:39:21 +0200] rev 23641
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm [Sat, 07 Jul 2007 18:39:20 +0200] rev 23640
toplevel prompt/print_state: proper markup, removed hooks;
tuned;
wenzelm [Sat, 07 Jul 2007 18:39:19 +0200] rev 23639
pretty_state: subgoal markup;
tuned;
wenzelm [Sat, 07 Jul 2007 18:39:18 +0200] rev 23638
added markup_chunks;
wenzelm [Sat, 07 Jul 2007 18:39:17 +0200] rev 23637
added toplevel markup;
misc cleanup;
wenzelm [Sat, 07 Jul 2007 18:39:16 +0200] rev 23636
use markup.ML earlier;
wenzelm [Sat, 07 Jul 2007 18:39:15 +0200] rev 23635
removed obsolete disable_pr/enable_pr;
added old print_goals from display.ML;
wenzelm [Sat, 07 Jul 2007 18:39:14 +0200] rev 23634
pretty_goals_aux: subgoal markup;
print_goals etc.: moved old version to old_goals.ML, removed hooks;
tuned;
wenzelm [Sat, 07 Jul 2007 18:39:12 +0200] rev 23633
pr_goals: adapted Display.pretty_goals_aux;
pr_goals/prterm: proper context;
tuned;
wenzelm [Sat, 07 Jul 2007 12:16:20 +0200] rev 23632
export attribute;
wenzelm [Sat, 07 Jul 2007 12:16:19 +0200] rev 23631
pretty_sort/typ/term: markup;
wenzelm [Sat, 07 Jul 2007 12:16:18 +0200] rev 23630
pretty: markup for syntax/name of authentic consts;
datatype symb: String (potential markup) vs. Space (no markup);
wenzelm [Sat, 07 Jul 2007 12:16:17 +0200] rev 23629
depend on alist.ML, markup.ML;
wenzelm [Sat, 07 Jul 2007 12:16:16 +0200] rev 23628
markup: emit as control information -- no indent text;
wenzelm [Sat, 07 Jul 2007 12:16:15 +0200] rev 23627
added property conversions;
tuned;
wenzelm [Sat, 07 Jul 2007 12:16:14 +0200] rev 23626
position: line and name;
tuned operations;
wenzelm [Sat, 07 Jul 2007 12:16:13 +0200] rev 23625
moved markup.ML before position.ML;
chaieb [Sat, 07 Jul 2007 11:09:40 +0200] rev 23624
The order for parameter for interpretation is now inversted:
f t env0 env1 ... envn = ...
where t is the type to be reified;
wenzelm [Sat, 07 Jul 2007 00:17:10 +0200] rev 23623
Common markup elements.
wenzelm [Sat, 07 Jul 2007 00:15:03 +0200] rev 23622
simplified pretty token metric: type int;
added command markup;
token translations: proper treatment of skolems;
separate print_mode setup for Output/Pretty;
wenzelm [Sat, 07 Jul 2007 00:15:02 +0200] rev 23621
simplified pretty token metric: type int;
separate print_mode setup for Output/Pretty;
wenzelm [Sat, 07 Jul 2007 00:15:02 +0200] rev 23620
moved General/xml.ML to Tools/xml.ML;
actually use pgml.ML;
wenzelm [Sat, 07 Jul 2007 00:15:00 +0200] rev 23619
tuned;
wenzelm [Sat, 07 Jul 2007 00:14:59 +0200] rev 23618
simplified output mode setup;
removed unused symbol_output;
tuned;
wenzelm [Sat, 07 Jul 2007 00:14:58 +0200] rev 23617
added print_mode setup: indent and markup;
simplified pretty token metric: type int;
added general markup for blocks;
removed unused writelns;
wenzelm [Sat, 07 Jul 2007 00:14:57 +0200] rev 23616
renamed raw to escape;
simplified pretty token metric: type int;
simplified print_mode setup: output_width and escape;
moved pretty setup to pretty.ML;
wenzelm [Sat, 07 Jul 2007 00:14:56 +0200] rev 23615
simplified pretty token metric: type int;
wenzelm [Sat, 07 Jul 2007 00:14:54 +0200] rev 23614
moved General/xml.ML to Tools/xml.ML;
wenzelm [Sat, 07 Jul 2007 00:14:52 +0200] rev 23613
added General/markup.ML;
moved General/xml.ML to Tools/xml.ML;
wenzelm [Sat, 07 Jul 2007 00:14:49 +0200] rev 23612
added class skolem, command;
nipkow [Fri, 06 Jul 2007 23:26:13 +0200] rev 23611
more interpretations
aspinall [Fri, 06 Jul 2007 17:52:52 +0200] rev 23610
Produce good PGML 2.0
webertj [Fri, 06 Jul 2007 17:21:18 +0200] rev 23609
cosmetic (line length fixed)
chaieb [Fri, 06 Jul 2007 16:09:28 +0200] rev 23608
Some examples for reifying type variables
chaieb [Fri, 06 Jul 2007 16:09:27 +0200] rev 23607
Tuned document
chaieb [Fri, 06 Jul 2007 16:09:26 +0200] rev 23606
Cleaned add and del attributes
chaieb [Fri, 06 Jul 2007 16:09:25 +0200] rev 23605
Reification now deals with type variables
wenzelm [Fri, 06 Jul 2007 11:55:05 +0200] rev 23604
Cumulative reports for Poly/ML profiling output.
aspinall [Thu, 05 Jul 2007 20:36:48 +0200] rev 23603
Update PGML version, add system name
wenzelm [Thu, 05 Jul 2007 20:01:39 +0200] rev 23602
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
removed atomize_cterm/goal;
wenzelm [Thu, 05 Jul 2007 20:01:38 +0200] rev 23601
added type conv;
merge_thys: removed dead exception handlers;
tuned;
wenzelm [Thu, 05 Jul 2007 20:01:37 +0200] rev 23600
removed comments -- no exception TERM;
merge_list: exception THEORY;
wenzelm [Thu, 05 Jul 2007 20:01:36 +0200] rev 23599
added is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:35 +0200] rev 23598
tuned;
wenzelm [Thu, 05 Jul 2007 20:01:34 +0200] rev 23597
simplified has_meta_prems;
wenzelm [Thu, 05 Jul 2007 20:01:33 +0200] rev 23596
moved type conv to thm.ML;
renamed Conv.is_refl to Thm.is_reflexive;
misc tuning of basic conversions;
wenzelm [Thu, 05 Jul 2007 20:01:32 +0200] rev 23595
the_theory/proof: error instead of exception Fail;
wenzelm [Thu, 05 Jul 2007 20:01:31 +0200] rev 23594
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
added flat_rule filter for addXXs etc.;
wenzelm [Thu, 05 Jul 2007 20:01:30 +0200] rev 23593
renamed Conv.is_refl to Thm.is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:29 +0200] rev 23592
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
simplified ObjectLogic.atomize;
wenzelm [Thu, 05 Jul 2007 20:01:28 +0200] rev 23591
simplified ObjectLogic.atomize;
wenzelm [Thu, 05 Jul 2007 20:01:26 +0200] rev 23590
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
aspinall [Thu, 05 Jul 2007 19:59:01 +0200] rev 23589
Revert body of pgml to match schema for now [change bad for Broker]
aspinall [Thu, 05 Jul 2007 19:57:19 +0200] rev 23588
Classify -- comments as ordinary comments (no undo)
wenzelm [Thu, 05 Jul 2007 00:15:44 +0200] rev 23587
tuned;
wenzelm [Thu, 05 Jul 2007 00:06:25 +0200] rev 23586
avoid polymorphic equality;
added dest_judgment;
wenzelm [Thu, 05 Jul 2007 00:06:24 +0200] rev 23585
sort_le: tuned eq case;
wenzelm [Thu, 05 Jul 2007 00:06:23 +0200] rev 23584
tuned goal conversion interfaces;
wenzelm [Thu, 05 Jul 2007 00:06:22 +0200] rev 23583
else_conv: only handle THM | CTERM | TERM | TYPE;
prems_conv: no index;
renamed goal_conv_rule to gconv_rule;
wenzelm [Thu, 05 Jul 2007 00:06:20 +0200] rev 23582
avoid polymorphic equality;
Numeral.mk_cnumber;
wenzelm [Thu, 05 Jul 2007 00:06:19 +0200] rev 23581
tuned;
wenzelm [Thu, 05 Jul 2007 00:06:18 +0200] rev 23580
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
tuned;
wenzelm [Thu, 05 Jul 2007 00:06:17 +0200] rev 23579
avoid polymorphic equality;
do not export ring_conv (which is not a conversion anyway);
renamed algebra_tac to ring_tac;
ring_tac: simplified tactic wrapper, no longer handles ERROR;
wenzelm [Thu, 05 Jul 2007 00:06:16 +0200] rev 23578
avoid polymorphic equality;
removed dead code;
wenzelm [Thu, 05 Jul 2007 00:06:14 +0200] rev 23577
avoid polymorphic equality;
wenzelm [Thu, 05 Jul 2007 00:06:13 +0200] rev 23576
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
wenzelm [Thu, 05 Jul 2007 00:06:12 +0200] rev 23575
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm [Thu, 05 Jul 2007 00:06:11 +0200] rev 23574
added Tools/numeral.ML;
wenzelm [Thu, 05 Jul 2007 00:06:10 +0200] rev 23573
common normalizer_funs, avoid cterm_of;
wenzelm [Thu, 05 Jul 2007 00:06:09 +0200] rev 23572
Numeral.mk_cnumber;
aspinall [Wed, 04 Jul 2007 21:20:23 +0200] rev 23571
PGML abstraction, draft version
aspinall [Wed, 04 Jul 2007 21:19:34 +0200] rev 23570
Use pgml
obua [Wed, 04 Jul 2007 17:21:02 +0200] rev 23569
fixed argument order in calls to Integer.pow
wenzelm [Wed, 04 Jul 2007 16:49:36 +0200] rev 23568
added binop_cong_rule;
wenzelm [Wed, 04 Jul 2007 16:49:35 +0200] rev 23567
export dlo_conv;
removed redundant auxiliary operations;
tuned exceptions -- avoid error here;
simplified tactic wrapper (CSUBGOAL, CONVERSION);
merge_ss: recover simpset context;
tuned;
wenzelm [Wed, 04 Jul 2007 16:49:34 +0200] rev 23566
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
nipkow [Wed, 04 Jul 2007 14:21:00 +0200] rev 23565
*** empty log message ***
nipkow [Wed, 04 Jul 2007 14:10:01 +0200] rev 23564
*** empty log message ***
paulson [Wed, 04 Jul 2007 13:56:26 +0200] rev 23563
simplified a proof
wenzelm [Tue, 03 Jul 2007 23:00:42 +0200] rev 23562
tuned;
wenzelm [Tue, 03 Jul 2007 22:27:30 +0200] rev 23561
CONVERSION: handle TYPE | TERM | CTERM | THM;
wenzelm [Tue, 03 Jul 2007 22:27:27 +0200] rev 23560
proper use of ioa_package.ML;
wenzelm [Tue, 03 Jul 2007 22:27:25 +0200] rev 23559
tuned;
wenzelm [Tue, 03 Jul 2007 22:27:19 +0200] rev 23558
tuned is_comb/is_binop -- avoid construction of cterms;
removed conjunction rules (cf. HOLogic.conj_XXX);
wenzelm [Tue, 03 Jul 2007 22:27:16 +0200] rev 23557
HOLogic.conj_intr/elims;
removed obsolete assocd/assoc;
removed dead string_of_pol;
tuned;
wenzelm [Tue, 03 Jul 2007 22:27:13 +0200] rev 23556
use mucke_oracle.ML only once;
wenzelm [Tue, 03 Jul 2007 22:27:11 +0200] rev 23555
assume basic HOL context for compilation (antiquotations);
added dest_cTrueprop;
tuned Trueprop_conv;
added low-level conj_intr/elim/elis (dire need for @{rule} antiquotation!);
wenzelm [Tue, 03 Jul 2007 22:27:08 +0200] rev 23554
proper use of function_package ML files;
wenzelm [Tue, 03 Jul 2007 22:27:05 +0200] rev 23553
use hologic.ML in basic HOL context;
tuned proofs;
paulson [Tue, 03 Jul 2007 21:56:25 +0200] rev 23552
to handle non-atomic assumptions
wenzelm [Tue, 03 Jul 2007 20:26:08 +0200] rev 23551
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
huffman [Tue, 03 Jul 2007 18:42:09 +0200] rev 23550
convert instance proofs to Isar style
chaieb [Tue, 03 Jul 2007 18:00:57 +0200] rev 23549
Dependency on reflection_data.ML to build HOL-ex
chaieb [Tue, 03 Jul 2007 17:50:00 +0200] rev 23548
Generalized case for atoms. Selection of environment lists is allowed more than once.
chaieb [Tue, 03 Jul 2007 17:49:58 +0200] rev 23547
More examples
chaieb [Tue, 03 Jul 2007 17:49:55 +0200] rev 23546
reflection and reification methods now manage Context data
chaieb [Tue, 03 Jul 2007 17:49:53 +0200] rev 23545
Context Data for the reflection and reification methods
huffman [Tue, 03 Jul 2007 17:28:36 +0200] rev 23544
rename class dom to ring_1_no_zero_divisors
wenzelm [Tue, 03 Jul 2007 17:17:17 +0200] rev 23543
rewrite_goal_tac;
wenzelm [Tue, 03 Jul 2007 17:17:16 +0200] rev 23542
replaced Conv.goals_conv by Conv.prems_conv;
wenzelm [Tue, 03 Jul 2007 17:17:15 +0200] rev 23541
exported meta_rewrite_conv;
CONVERSION tactical;
wenzelm [Tue, 03 Jul 2007 17:17:15 +0200] rev 23540
CONVERSION tactical;
MetaSimplifier.rewrite_goal_tac;
wenzelm [Tue, 03 Jul 2007 17:17:13 +0200] rev 23539
removed obsolete eta_long_tac;
wenzelm [Tue, 03 Jul 2007 17:17:13 +0200] rev 23538
added CONVERSION tactical;
tuned signature;
wenzelm [Tue, 03 Jul 2007 17:17:11 +0200] rev 23537
tuned rotate_prems;
tuned comments;
wenzelm [Tue, 03 Jul 2007 17:17:11 +0200] rev 23536
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
wenzelm [Tue, 03 Jul 2007 17:17:09 +0200] rev 23535
removed obsolete mk_conjunction_list, intr/elim_list;
wenzelm [Tue, 03 Jul 2007 17:17:09 +0200] rev 23534
removed obsolete goals_conv (cf. prems_conv);
added efficient goal_conv_rule;
tuned comments;
wenzelm [Tue, 03 Jul 2007 17:17:07 +0200] rev 23533
Conjunction.intr/elim_balanced;
CONVERSION tactical;
tuned;
wenzelm [Tue, 03 Jul 2007 17:17:07 +0200] rev 23532
CONVERSION tactical;
Simplifier.rewrite_goal_tac;
wenzelm [Tue, 03 Jul 2007 17:17:06 +0200] rev 23531
Conjunction.mk_conjunction_balanced;
wenzelm [Tue, 03 Jul 2007 17:17:04 +0200] rev 23530
CONVERSION tactical;
nipkow [Tue, 03 Jul 2007 15:23:11 +0200] rev 23529
Fixed problem with patterns in lambdas
krauss [Tue, 03 Jul 2007 14:48:27 +0200] rev 23528
fixed an issue with mutual recursion
huffman [Tue, 03 Jul 2007 01:26:06 +0200] rev 23527
instance pordered_comm_ring < pordered_ring
nipkow [Mon, 02 Jul 2007 23:14:06 +0200] rev 23526
Added pattern maatching for lambda abstraction
paulson [Mon, 02 Jul 2007 16:42:37 +0200] rev 23525
revised the discussion of type classes
chaieb [Mon, 02 Jul 2007 10:43:20 +0200] rev 23524
Generic QE need no Context anymore
chaieb [Mon, 02 Jul 2007 10:43:19 +0200] rev 23523
Handle exception TYPE
chaieb [Mon, 02 Jul 2007 10:43:17 +0200] rev 23522
Tuned proofs
obua [Sat, 30 Jun 2007 17:30:10 +0200] rev 23521
added ordered_ring and ordered_semiring
haftmann [Fri, 29 Jun 2007 21:23:05 +0200] rev 23520
tuned arithmetic modules
paulson [Fri, 29 Jun 2007 18:21:25 +0200] rev 23519
bug fixes to proof reconstruction
haftmann [Fri, 29 Jun 2007 16:05:00 +0200] rev 23518
dropped local cg cmd
haftmann [Thu, 28 Jun 2007 19:09:43 +0200] rev 23517
dropped toplevel lcm, gcd
haftmann [Thu, 28 Jun 2007 19:09:41 +0200] rev 23516
proper collapse_let
haftmann [Thu, 28 Jun 2007 19:09:38 +0200] rev 23515
new code generator framework
haftmann [Thu, 28 Jun 2007 19:09:36 +0200] rev 23514
dropped Library.lcm
haftmann [Thu, 28 Jun 2007 19:09:35 +0200] rev 23513
tuned
haftmann [Thu, 28 Jun 2007 19:09:34 +0200] rev 23512
code generation for dvd
haftmann [Thu, 28 Jun 2007 19:09:32 +0200] rev 23511
simplified keyword setup
paulson [Wed, 27 Jun 2007 12:41:36 +0200] rev 23510
GPL -> BSD
nipkow [Wed, 27 Jun 2007 11:06:43 +0200] rev 23509
*** empty log message ***
paulson [Tue, 26 Jun 2007 18:32:53 +0200] rev 23508
updated for metis method
paulson [Tue, 26 Jun 2007 18:32:24 +0200] rev 23507
recoded
paulson [Tue, 26 Jun 2007 18:28:40 +0200] rev 23506
simplified
paulson [Tue, 26 Jun 2007 15:48:24 +0200] rev 23505
completed some references
paulson [Tue, 26 Jun 2007 15:48:09 +0200] rev 23504
changes for type class ring_no_zero_divisors
nipkow [Tue, 26 Jun 2007 13:02:28 +0200] rev 23503
*** empty log message ***
nipkow [Tue, 26 Jun 2007 13:01:48 +0200] rev 23502
added NBE
nipkow [Tue, 26 Jun 2007 08:42:04 +0200] rev 23501
removed removed lemmas
wenzelm [Tue, 26 Jun 2007 00:35:14 +0200] rev 23500
fixed undo: try undos_proof first!
wenzelm [Mon, 25 Jun 2007 22:46:55 +0200] rev 23499
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
eta_long_tac;
tuned;
nipkow [Mon, 25 Jun 2007 16:56:41 +0200] rev 23498
removed theorem
nipkow [Mon, 25 Jun 2007 15:19:34 +0200] rev 23497
removed redundant lemma
nipkow [Mon, 25 Jun 2007 15:19:18 +0200] rev 23496
removed redundant lemmas
obua [Mon, 25 Jun 2007 14:49:32 +0200] rev 23495
commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
krauss [Mon, 25 Jun 2007 12:16:27 +0200] rev 23494
removed "sum_tools.ML" in favour of BalancedTree
wenzelm [Mon, 25 Jun 2007 00:36:42 +0200] rev 23493
added eta_long_conversion;
wenzelm [Mon, 25 Jun 2007 00:36:41 +0200] rev 23492
added eta_long_tac;
wenzelm [Mon, 25 Jun 2007 00:36:40 +0200] rev 23491
added reasonably efficient add_cterm_frees;
wenzelm [Mon, 25 Jun 2007 00:36:39 +0200] rev 23490
made type conv pervasive;
removed obsolete eta_conv (cf. Thm.eta_long_conv);
wenzelm [Mon, 25 Jun 2007 00:36:38 +0200] rev 23489
made type conv pervasive;
Thm.eta_long_conversion;
Thm.add_cterm_frees;
tuned;
wenzelm [Mon, 25 Jun 2007 00:36:37 +0200] rev 23488
Thm.eta_long_conversion;
wenzelm [Mon, 25 Jun 2007 00:36:36 +0200] rev 23487
made type conv pervasive;
Thm.add_cterm_frees;
wenzelm [Mon, 25 Jun 2007 00:36:35 +0200] rev 23486
Thm.add_cterm_frees;
wenzelm [Mon, 25 Jun 2007 00:36:34 +0200] rev 23485
made type conv pervasive;
wenzelm [Mon, 25 Jun 2007 00:36:33 +0200] rev 23484
made type conv pervasive;
tuned;
nipkow [Sun, 24 Jun 2007 21:15:55 +0200] rev 23483
tex problem fixed
nipkow [Sun, 24 Jun 2007 20:55:41 +0200] rev 23482
tuned and used field_simps
nipkow [Sun, 24 Jun 2007 20:47:05 +0200] rev 23481
*** empty log message ***
nipkow [Sun, 24 Jun 2007 20:18:20 +0200] rev 23480
*** empty log message ***
nipkow [Sun, 24 Jun 2007 15:17:54 +0200] rev 23479
new lemmas
nipkow [Sun, 24 Jun 2007 10:33:49 +0200] rev 23478
*** empty log message ***
nipkow [Sat, 23 Jun 2007 19:33:22 +0200] rev 23477
tuned and renamed group_eq_simps and ring_eq_simps
huffman [Fri, 22 Jun 2007 22:41:17 +0200] rev 23476
fix looping simp rule
huffman [Fri, 22 Jun 2007 20:19:39 +0200] rev 23475
reinstate real_root_less_iff [simp]
chaieb [Fri, 22 Jun 2007 16:16:23 +0200] rev 23474
merge is now identity
krauss [Fri, 22 Jun 2007 10:23:37 +0200] rev 23473
new method "elim_to_cases" provides ad-hoc conversion of obtain-style
elimination goals to a disjunction of existentials.
huffman [Thu, 21 Jun 2007 23:49:26 +0200] rev 23472
section headings
huffman [Thu, 21 Jun 2007 23:33:10 +0200] rev 23471
add thm antiquotations
huffman [Thu, 21 Jun 2007 23:28:44 +0200] rev 23470
spelling
huffman [Thu, 21 Jun 2007 22:52:22 +0200] rev 23469
add thm antiquotations
huffman [Thu, 21 Jun 2007 22:30:58 +0200] rev 23468
changed simp rules for of_nat
wenzelm [Thu, 21 Jun 2007 22:10:16 +0200] rev 23467
tuned proofs -- avoid implicit prems;
wenzelm [Thu, 21 Jun 2007 20:48:48 +0200] rev 23466
moved quantifier elimination tools to Tools/Qelim/;
wenzelm [Thu, 21 Jun 2007 20:48:47 +0200] rev 23465
moved Presburger setup back to Presburger.thy;
wenzelm [Thu, 21 Jun 2007 20:07:26 +0200] rev 23464
tuned proofs -- avoid implicit prems;
wenzelm [Thu, 21 Jun 2007 17:28:53 +0200] rev 23463
tuned proofs -- avoid implicit prems;
wenzelm [Thu, 21 Jun 2007 17:28:50 +0200] rev 23462
renamed NatSimprocs.thy to Arith_Tools.thy;
incorporated HOL/Presburger.thy into NatSimprocs.thy;
wenzelm [Thu, 21 Jun 2007 15:42:15 +0200] rev 23461
tuned;
wenzelm [Thu, 21 Jun 2007 15:42:14 +0200] rev 23460
adapted tool setup;
wenzelm [Thu, 21 Jun 2007 15:42:13 +0200] rev 23459
added Ferrante-Rackoff setup;
wenzelm [Thu, 21 Jun 2007 15:42:12 +0200] rev 23458
tuned comments;
wenzelm [Thu, 21 Jun 2007 15:42:11 +0200] rev 23457
moved HOL/Tools/Presburger/qelim.ML to HOL/Tools/qelim.ML;
wenzelm [Thu, 21 Jun 2007 15:42:10 +0200] rev 23456
Ferrante-Rackoff quantifier elimination.
wenzelm [Thu, 21 Jun 2007 15:42:09 +0200] rev 23455
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm [Thu, 21 Jun 2007 15:42:07 +0200] rev 23454
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm [Thu, 21 Jun 2007 15:42:06 +0200] rev 23453
Dense linear order witout endpoints
and a quantifier elimination procedure in Ferrante and Rackoff style.
wenzelm [Thu, 21 Jun 2007 13:53:53 +0200] rev 23452
renamed metis-env.ML to metis_env.ML;
wenzelm [Thu, 21 Jun 2007 13:53:23 +0200] rev 23451
added Id;
narboux [Thu, 21 Jun 2007 13:49:27 +0200] rev 23450
fine tune automatic generation of inversion lemmas
paulson [Thu, 21 Jun 2007 13:23:33 +0200] rev 23449
integration of Metis prover
wenzelm [Thu, 21 Jun 2007 12:01:27 +0200] rev 23448
renamed metis-env to metis-env.ML;
wenzelm [Wed, 20 Jun 2007 23:19:18 +0200] rev 23447
tuned comments;
wenzelm [Wed, 20 Jun 2007 23:19:17 +0200] rev 23446
obsolete (cf. ATP_Linkup.thy);
wenzelm [Wed, 20 Jun 2007 23:19:17 +0200] rev 23445
added Tools/metis_tools.ML;
wenzelm [Wed, 20 Jun 2007 23:19:16 +0200] rev 23444
added Metis setup (from Metis.thy);
wenzelm [Wed, 20 Jun 2007 23:15:25 +0200] rev 23443
added HOL-Nominal-Examples;
wenzelm [Wed, 20 Jun 2007 22:07:52 +0200] rev 23442
The Metis prover (slightly modified version from Larry);
huffman [Wed, 20 Jun 2007 19:49:14 +0200] rev 23441
avoid using implicit prems in assumption
paulson [Wed, 20 Jun 2007 17:34:44 +0200] rev 23440
Added flexflex_first_order and tidied first_order_resolution
paulson [Wed, 20 Jun 2007 17:32:53 +0200] rev 23439
A more robust flexflex_unique
huffman [Wed, 20 Jun 2007 17:28:55 +0200] rev 23438
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
krauss [Wed, 20 Jun 2007 17:02:57 +0200] rev 23437
tuned error msg
aspinall [Wed, 20 Jun 2007 15:10:34 +0200] rev 23436
Remove dedicated flag setting elements in favour of setproverflag.
aspinall [Wed, 20 Jun 2007 15:10:02 +0200] rev 23435
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall [Wed, 20 Jun 2007 15:07:42 +0200] rev 23434
Synchronize schema with current version
nipkow [Wed, 20 Jun 2007 14:38:24 +0200] rev 23433
added lemmas
nipkow [Wed, 20 Jun 2007 08:09:56 +0200] rev 23432
added meta_impE
huffman [Wed, 20 Jun 2007 05:18:39 +0200] rev 23431
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman [Wed, 20 Jun 2007 05:06:56 +0200] rev 23430
section headings
huffman [Wed, 20 Jun 2007 05:06:16 +0200] rev 23429
simplify some proofs
wenzelm [Tue, 19 Jun 2007 23:21:39 +0200] rev 23428
oops -- fixed profiling;
wenzelm [Tue, 19 Jun 2007 23:16:14 +0200] rev 23427
Balanced binary trees (material from library.ML);
wenzelm [Tue, 19 Jun 2007 23:15:59 +0200] rev 23426
profiling: observe no_timing;
wenzelm [Tue, 19 Jun 2007 23:15:57 +0200] rev 23425
added raw_tactic;
wenzelm [Tue, 19 Jun 2007 23:15:54 +0200] rev 23424
moved balanced tree operations to General/balanced_tree.ML;
wenzelm [Tue, 19 Jun 2007 23:15:51 +0200] rev 23423
added with_subgoal;
wenzelm [Tue, 19 Jun 2007 23:15:49 +0200] rev 23422
balanced conjunctions;
tuned interfaces;
tuned;
wenzelm [Tue, 19 Jun 2007 23:15:47 +0200] rev 23421
balanced conjunctions;
added split_defined (from conjunction.ML);
wenzelm [Tue, 19 Jun 2007 23:15:43 +0200] rev 23420
added General/balanced_tree.ML;
wenzelm [Tue, 19 Jun 2007 23:15:38 +0200] rev 23419
BalancedTree;
wenzelm [Tue, 19 Jun 2007 23:15:27 +0200] rev 23418
balanced conjunctions;
wenzelm [Tue, 19 Jun 2007 23:15:23 +0200] rev 23417
tuned;
krauss [Tue, 19 Jun 2007 18:00:49 +0200] rev 23416
generalized proofs so that call graphs can have any node type.
wenzelm [Tue, 19 Jun 2007 00:02:16 +0200] rev 23415
macbroy5: trying -j 2;
wenzelm [Mon, 18 Jun 2007 23:30:46 +0200] rev 23414
tuned conjunction tactics: slightly smaller proof terms;
nipkow [Sun, 17 Jun 2007 18:47:03 +0200] rev 23413
tuned laws for cancellation in divisions for fields.
chaieb [Sun, 17 Jun 2007 13:39:50 +0200] rev 23412
moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs
chaieb [Sun, 17 Jun 2007 13:39:48 +0200] rev 23411
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
chaieb [Sun, 17 Jun 2007 13:39:45 +0200] rev 23410
gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;
chaieb [Sun, 17 Jun 2007 13:39:39 +0200] rev 23409
thin_prems_tac first max-scopes universal quantifiers; eta_conv moved to Pure/conv.ML
chaieb [Sun, 17 Jun 2007 13:39:34 +0200] rev 23408
Tuned error messages; tuned;
chaieb [Sun, 17 Jun 2007 13:39:32 +0200] rev 23407
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb [Sun, 17 Jun 2007 13:39:29 +0200] rev 23406
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb [Sun, 17 Jun 2007 13:39:27 +0200] rev 23405
moved lemma all_not_ex to HOL.thy ; tuned proofs
chaieb [Sun, 17 Jun 2007 13:39:25 +0200] rev 23404
Tuned instantiation of Groebner bases to fields
chaieb [Sun, 17 Jun 2007 13:39:22 +0200] rev 23403
added Theorem all_not_ex
nipkow [Sun, 17 Jun 2007 08:56:13 +0200] rev 23402
renamed vars in zle_trans for compatibility
nipkow [Sat, 16 Jun 2007 16:27:35 +0200] rev 23401
tuned
nipkow [Sat, 16 Jun 2007 15:01:54 +0200] rev 23400
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
longer need class numeral_ring. This made a number of special
simp-thms redundant.
berghofe [Fri, 15 Jun 2007 19:19:23 +0200] rev 23399
Locally added definition of "int :: nat => int" again to make
code generation work.
nipkow [Fri, 15 Jun 2007 15:10:32 +0200] rev 23398
made divide_self a simp rule
nipkow [Fri, 15 Jun 2007 09:10:06 +0200] rev 23397
Removed thunk from Fun
nipkow [Fri, 15 Jun 2007 09:09:06 +0200] rev 23396
Church numerals added
wenzelm [Thu, 14 Jun 2007 23:04:40 +0200] rev 23395
method assumption: uniform treatment of prems as legacy feature;
wenzelm [Thu, 14 Jun 2007 23:04:39 +0200] rev 23394
tuned proofs;
wenzelm [Thu, 14 Jun 2007 23:04:36 +0200] rev 23393
tuned proofs: avoid implicit prems;
chaieb [Thu, 14 Jun 2007 22:59:42 +0200] rev 23392
fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)
chaieb [Thu, 14 Jun 2007 22:59:40 +0200] rev 23391
no computation rules in the pre-simplifiaction set
chaieb [Thu, 14 Jun 2007 22:59:39 +0200] rev 23390
Added some lemmas to default presburger simpset; tuned proofs
wenzelm [Thu, 14 Jun 2007 18:33:31 +0200] rev 23389
tuned proofs: avoid implicit prems;
wenzelm [Thu, 14 Jun 2007 18:33:29 +0200] rev 23388
tuned proofs: avoid implicit prems;
tuned partition proofs;
paulson [Thu, 14 Jun 2007 13:19:50 +0200] rev 23387
Now ResHolClause also does first-order problems!
paulson [Thu, 14 Jun 2007 13:18:59 +0200] rev 23386
Now also handles FO problems
paulson [Thu, 14 Jun 2007 13:18:24 +0200] rev 23385
Deleted unused code
paulson [Thu, 14 Jun 2007 13:16:44 +0200] rev 23384
tidied
wenzelm [Thu, 14 Jun 2007 10:38:48 +0200] rev 23383
tuned proofs: avoid implicit prems;
kleing [Thu, 14 Jun 2007 09:54:14 +0200] rev 23382
clarified who we consider to be a contributor
chaieb [Thu, 14 Jun 2007 09:37:38 +0200] rev 23381
Fixed Problem with ML-bindings for thm names;
nipkow [Thu, 14 Jun 2007 07:27:55 +0200] rev 23380
fixed filter syntax
wenzelm [Thu, 14 Jun 2007 00:48:42 +0200] rev 23379
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm [Thu, 14 Jun 2007 00:22:45 +0200] rev 23378
tuned proofs: avoid implicit prems;
huffman [Wed, 13 Jun 2007 19:14:51 +0200] rev 23377
int abbreviates of_nat
wenzelm [Wed, 13 Jun 2007 18:30:17 +0200] rev 23376
tuned proofs: avoid implicit prems;
tuned;
wenzelm [Wed, 13 Jun 2007 18:30:16 +0200] rev 23375
tuned proofs: avoid implicit prems;
major cleanup of proofs/document;
wenzelm [Wed, 13 Jun 2007 18:30:15 +0200] rev 23374
tuned comments;
wenzelm [Wed, 13 Jun 2007 18:30:11 +0200] rev 23373
tuned proofs: avoid implicit prems;
huffman [Wed, 13 Jun 2007 16:43:02 +0200] rev 23372
clean up instance proofs; reorganize section headings
wenzelm [Wed, 13 Jun 2007 14:21:54 +0200] rev 23371
reactivated theory Class;
urbanc [Wed, 13 Jun 2007 12:22:02 +0200] rev 23370
added the Q_Unit rule (was missing) and adjusted the proof accordingly
wenzelm [Wed, 13 Jun 2007 11:54:03 +0200] rev 23369
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
* Isar: implicit use of prems from the Isar proof context is considered a legacy feature;
narboux [Wed, 13 Jun 2007 11:16:24 +0200] rev 23368
generate_fresh works even if there is no free variable in the goal
wenzelm [Wed, 13 Jun 2007 10:44:35 +0200] rev 23367
tuned;
wenzelm [Wed, 13 Jun 2007 10:43:38 +0200] rev 23366
tuned proofs: avoid implicit prems;
huffman [Wed, 13 Jun 2007 03:31:11 +0200] rev 23365
removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int
huffman [Wed, 13 Jun 2007 03:28:21 +0200] rev 23364
thm antiquotations
wenzelm [Wed, 13 Jun 2007 00:02:06 +0200] rev 23363
transaction: context_position (non-destructive only);
wenzelm [Wed, 13 Jun 2007 00:02:05 +0200] rev 23362
added map_current;
simplified internal type proof;
wenzelm [Wed, 13 Jun 2007 00:02:04 +0200] rev 23361
tuned msg;
wenzelm [Wed, 13 Jun 2007 00:02:03 +0200] rev 23360
apply_method/end_proof: pass position;
Method.Basic: include position;
wenzelm [Wed, 13 Jun 2007 00:02:02 +0200] rev 23359
renamed map to map_current;
wenzelm [Wed, 13 Jun 2007 00:02:01 +0200] rev 23358
tuned;
wenzelm [Wed, 13 Jun 2007 00:02:00 +0200] rev 23357
removed unused is_atomic;
wenzelm [Wed, 13 Jun 2007 00:01:59 +0200] rev 23356
renamed prove_raw to prove_internal;
tuned;
wenzelm [Wed, 13 Jun 2007 00:01:58 +0200] rev 23355
merge/merge_refs: plain error instead of exception TERM;
wenzelm [Wed, 13 Jun 2007 00:01:57 +0200] rev 23354
Context positions.
wenzelm [Wed, 13 Jun 2007 00:01:56 +0200] rev 23353
added context_position.ML;
wenzelm [Wed, 13 Jun 2007 00:01:54 +0200] rev 23352
renamed Goal.prove_raw to Goal.prove_internal;
wenzelm [Wed, 13 Jun 2007 00:01:51 +0200] rev 23351
Method.Basic: include position;
wenzelm [Wed, 13 Jun 2007 00:01:41 +0200] rev 23350
tuned proofs: avoid implicit prems;
wenzelm [Wed, 13 Jun 2007 00:01:38 +0200] rev 23349
Basic text: include position;
assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;
huffman [Tue, 12 Jun 2007 23:39:02 +0200] rev 23348
thm antiquotations
huffman [Tue, 12 Jun 2007 23:14:29 +0200] rev 23347
add lemma inj_of_nat
huffman [Tue, 12 Jun 2007 21:59:40 +0200] rev 23346
thm antiquotations
chaieb [Tue, 12 Jun 2007 20:49:56 +0200] rev 23345
Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns
chaieb [Tue, 12 Jun 2007 20:49:50 +0200] rev 23344
changed int stuff into integer for SMLNJ compatibility
huffman [Tue, 12 Jun 2007 17:20:30 +0200] rev 23343
more of_rat lemmas
huffman [Tue, 12 Jun 2007 17:04:26 +0200] rev 23342
add function of_rat and related lemmas
chaieb [Tue, 12 Jun 2007 12:00:03 +0200] rev 23341
turned curry (op opr) into curry op opr --- because of smlnj
wenzelm [Tue, 12 Jun 2007 11:01:16 +0200] rev 23340
De-overloaded operations for int and real.
wenzelm [Tue, 12 Jun 2007 11:00:18 +0200] rev 23339
SML basis with type int representing proper integers, not machine words.
chaieb [Tue, 12 Jun 2007 10:40:44 +0200] rev 23338
Tuned proofs : now use 'algebra ad: ...'
chaieb [Tue, 12 Jun 2007 10:15:58 +0200] rev 23337
cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification
chaieb [Tue, 12 Jun 2007 10:15:52 +0200] rev 23336
changed val restriction to local due to smlnj
chaieb [Tue, 12 Jun 2007 10:15:48 +0200] rev 23335
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb [Tue, 12 Jun 2007 10:15:45 +0200] rev 23334
Added algebra_tac; tuned;
chaieb [Tue, 12 Jun 2007 10:15:40 +0200] rev 23333
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
chaieb [Tue, 12 Jun 2007 10:15:32 +0200] rev 23332
algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
nipkow [Mon, 11 Jun 2007 18:34:12 +0200] rev 23331
nex example
chaieb [Mon, 11 Jun 2007 18:28:16 +0200] rev 23330
Conversion for computation on constants now depends on the context
chaieb [Mon, 11 Jun 2007 18:28:15 +0200] rev 23329
tuned setup for the fields instantiation for Groebner Bases;
chaieb [Mon, 11 Jun 2007 18:26:44 +0200] rev 23328
Added dependency on file Groebner_Basis.thy
chaieb [Mon, 11 Jun 2007 16:23:17 +0200] rev 23327
Added instantiation of algebra method to fields
nipkow [Mon, 11 Jun 2007 16:21:03 +0200] rev 23326
hid constant "dom"
chaieb [Mon, 11 Jun 2007 11:10:04 +0200] rev 23325
Removed from CVS, since obselete in the new Presburger Method;
chaieb [Mon, 11 Jun 2007 11:07:18 +0200] rev 23324
Generated reflected QE procedure for Presburger Arithmetic-- Cooper's Algorithm -- see HOL/ex/Reflected_Presburger.thy
chaieb [Mon, 11 Jun 2007 11:06:23 +0200] rev 23323
Added more examples
chaieb [Mon, 11 Jun 2007 11:06:21 +0200] rev 23322
Now only contains generic conversion for quantifier elimination in HOL
chaieb [Mon, 11 Jun 2007 11:06:19 +0200] rev 23321
A new tactic for Presburger;
chaieb [Mon, 11 Jun 2007 11:06:18 +0200] rev 23320
tuned
chaieb [Mon, 11 Jun 2007 11:06:17 +0200] rev 23319
Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;
chaieb [Mon, 11 Jun 2007 11:06:15 +0200] rev 23318
tuned tactic
chaieb [Mon, 11 Jun 2007 11:06:13 +0200] rev 23317
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed
chaieb [Mon, 11 Jun 2007 11:06:11 +0200] rev 23316
tuned Proof and Document
chaieb [Mon, 11 Jun 2007 11:06:04 +0200] rev 23315
tuned Proof
chaieb [Mon, 11 Jun 2007 11:06:00 +0200] rev 23314
A new and cleaned up Theory for QE. for Presburger arithmetic
chaieb [Mon, 11 Jun 2007 11:05:59 +0200] rev 23313
Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
chaieb [Mon, 11 Jun 2007 11:05:57 +0200] rev 23312
explicitely depends on file groebner.ML
chaieb [Mon, 11 Jun 2007 11:05:56 +0200] rev 23311
Context Data for the new presburger Method
chaieb [Mon, 11 Jun 2007 11:05:54 +0200] rev 23310
A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm
huffman [Mon, 11 Jun 2007 07:10:06 +0200] rev 23309
remove references to constant int::nat=>int
huffman [Mon, 11 Jun 2007 06:14:32 +0200] rev 23308
simplify int proofs
huffman [Mon, 11 Jun 2007 05:20:05 +0200] rev 23307
modify proofs to avoid referring to int::nat=>int
huffman [Mon, 11 Jun 2007 02:25:55 +0200] rev 23306
add int_of_nat versions of lemmas about int::nat=>int
huffman [Mon, 11 Jun 2007 02:24:39 +0200] rev 23305
add lemma of_nat_power
huffman [Mon, 11 Jun 2007 01:22:29 +0200] rev 23304
add int_of_nat versions of lemmas about int::nat=>int
huffman [Mon, 11 Jun 2007 00:53:18 +0200] rev 23303
add abbreviation int_of_nat for of_nat::nat=>int;
add int_of_nat versions of all lemmas about int::nat=>int;
move int lemmas into their own section, preparing to remove
wenzelm [Sun, 10 Jun 2007 23:48:27 +0200] rev 23302
disabled theory "Reflected_Presburger" for smlnj (temporarily);
wenzelm [Sun, 10 Jun 2007 21:06:59 +0200] rev 23301
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
nipkow [Sun, 10 Jun 2007 10:23:42 +0200] rev 23300
*** empty log message ***
huffman [Sat, 09 Jun 2007 02:38:51 +0200] rev 23299
remove dependencies of proofs on constant int::nat=>int, preparing to remove it
wenzelm [Sat, 09 Jun 2007 00:28:47 +0200] rev 23298
eqtype int -- explicitly encourage overloaded equality;
tuned -%;
removed obsolete Intt;
wenzelm [Sat, 09 Jun 2007 00:28:46 +0200] rev 23297
simplified type integer;
berghofe [Fri, 08 Jun 2007 18:13:58 +0200] rev 23296
Adapted Proofterm.bicompose_proof to Larry's changes in
Logic.assum_pairs from 2005-01-24 (revision 1.44).
chaieb [Fri, 08 Jun 2007 18:09:37 +0200] rev 23295
Method "algebra" solves polynomial equations over (semi)rings
huffman [Fri, 08 Jun 2007 03:24:27 +0200] rev 23294
generalize zpower_number_of_{even,odd} lemmas
obua [Thu, 07 Jun 2007 17:21:43 +0200] rev 23293
deleted comments
obua [Thu, 07 Jun 2007 14:26:05 +0200] rev 23292
deleted legacy lemmas
nipkow [Thu, 07 Jun 2007 11:25:27 +0200] rev 23291
somebody elses problem fixed
nipkow [Thu, 07 Jun 2007 11:25:05 +0200] rev 23290
filter syntax change
huffman [Thu, 07 Jun 2007 04:33:15 +0200] rev 23289
remove redundant lemmas
huffman [Thu, 07 Jun 2007 03:45:56 +0200] rev 23288
remove references to preal-specific theorems
huffman [Thu, 07 Jun 2007 03:11:31 +0200] rev 23287
define (1::preal); clean up instance declarations
huffman [Thu, 07 Jun 2007 02:34:37 +0200] rev 23286
tuned
huffman [Thu, 07 Jun 2007 01:44:35 +0200] rev 23285
instance preal :: ordered_cancel_ab_semigroup_add
huffman [Wed, 06 Jun 2007 23:06:29 +0200] rev 23284
use new-style class for sq_ord; rename op << to sq_le
urbanc [Wed, 06 Jun 2007 21:24:35 +0200] rev 23283
take out Class.thy again, because it does not yet compile cleanly
huffman [Wed, 06 Jun 2007 20:49:04 +0200] rev 23282
add axclass semiring_char_0 for types where of_nat is injective
nipkow [Wed, 06 Jun 2007 19:12:59 +0200] rev 23281
changed filter syntax from : to <-
nipkow [Wed, 06 Jun 2007 19:12:40 +0200] rev 23280
hide filter
nipkow [Wed, 06 Jun 2007 19:12:07 +0200] rev 23279
tuned list comprehension, changed filter syntax from : to <-
huffman [Wed, 06 Jun 2007 18:32:05 +0200] rev 23278
clean up proofs of exp_zero, sin_zero, cos_zero
huffman [Wed, 06 Jun 2007 17:01:33 +0200] rev 23277
generalize class constraints on some lemmas
huffman [Wed, 06 Jun 2007 17:00:09 +0200] rev 23276
generalize of_nat and related constants to class semiring_1
huffman [Wed, 06 Jun 2007 16:42:39 +0200] rev 23275
declare complex_diff as simp rule
chaieb [Wed, 06 Jun 2007 16:12:08 +0200] rev 23274
New Reflected Presburger added to HOL/ex
wenzelm [Tue, 05 Jun 2007 22:47:49 +0200] rev 23273
Groebner Basis Examples.
wenzelm [Tue, 05 Jun 2007 22:46:59 +0200] rev 23272
print_antiquotations: sort_strings;
wenzelm [Tue, 05 Jun 2007 22:46:58 +0200] rev 23271
tuned document;
added Groebner_Examples;
wenzelm [Tue, 05 Jun 2007 22:46:57 +0200] rev 23270
tuned source deps;
wenzelm [Tue, 05 Jun 2007 22:46:56 +0200] rev 23269
simplified/renamed add_numerals;
wenzelm [Tue, 05 Jun 2007 22:46:55 +0200] rev 23268
renamed ex/Eval_Examples.thy;
wenzelm [Tue, 05 Jun 2007 22:46:55 +0200] rev 23267
added ex/Groebner_Examples.thy;
renamed ex/Eval_Examples.thy;
wenzelm [Tue, 05 Jun 2007 22:46:53 +0200] rev 23266
tuned document;
chaieb [Tue, 05 Jun 2007 20:46:25 +0200] rev 23265
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
chaieb [Tue, 05 Jun 2007 20:44:12 +0200] rev 23264
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
haftmann [Tue, 05 Jun 2007 19:23:09 +0200] rev 23263
tuned boostrap
haftmann [Tue, 05 Jun 2007 19:22:01 +0200] rev 23262
eliminated Code_Generator.thy
haftmann [Tue, 05 Jun 2007 19:19:30 +0200] rev 23261
tuned integers
wenzelm [Tue, 05 Jun 2007 18:36:10 +0200] rev 23260
tuned;
wenzelm [Tue, 05 Jun 2007 18:36:09 +0200] rev 23259
fixed type int vs. integer;
wenzelm [Tue, 05 Jun 2007 18:36:07 +0200] rev 23258
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
huffman [Tue, 05 Jun 2007 17:16:41 +0200] rev 23257
add new lemmas
chaieb [Tue, 05 Jun 2007 16:32:16 +0200] rev 23256
Polynomials now only depend on Deriv; Definition of degree changed
chaieb [Tue, 05 Jun 2007 16:31:10 +0200] rev 23255
lemma lemma_DERIV_subst moved to Deriv.thy
wenzelm [Tue, 05 Jun 2007 16:26:07 +0200] rev 23254
tuned proofs;
wenzelm [Tue, 05 Jun 2007 16:26:06 +0200] rev 23253
tuned comments;
wenzelm [Tue, 05 Jun 2007 16:26:04 +0200] rev 23252
Semiring normalization and Groebner Bases.
haftmann [Tue, 05 Jun 2007 15:17:02 +0200] rev 23251
moved generic algebra modules
haftmann [Tue, 05 Jun 2007 15:16:11 +0200] rev 23250
updated documentation
haftmann [Tue, 05 Jun 2007 15:16:10 +0200] rev 23249
fixed broken execption handling
haftmann [Tue, 05 Jun 2007 15:16:09 +0200] rev 23248
simplified notion of "operational classes"
haftmann [Tue, 05 Jun 2007 15:16:08 +0200] rev 23247
merged Code_Generator.thy into HOL.thy
chaieb [Tue, 05 Jun 2007 12:12:25 +0200] rev 23246
added a function partition and a few lemmas
chaieb [Tue, 05 Jun 2007 11:00:04 +0200] rev 23245
added a few theorems about foldl and set
chaieb [Tue, 05 Jun 2007 10:42:31 +0200] rev 23244
added lcm, ilcm (lcm for integers) and some lemmas about them;
urbanc [Tue, 05 Jun 2007 09:56:19 +0200] rev 23243
included Class.thy in the compiling process for Nominal/Examples
huffman [Tue, 05 Jun 2007 07:58:50 +0200] rev 23242
remove simp attribute from lemma_STAR theorems
huffman [Tue, 05 Jun 2007 00:54:03 +0200] rev 23241
add lemma exp_of_real
nipkow [Mon, 04 Jun 2007 22:27:18 +0200] rev 23240
tuned list comprehension
wenzelm [Mon, 04 Jun 2007 21:04:20 +0200] rev 23239
tuned;
wenzelm [Mon, 04 Jun 2007 21:04:19 +0200] rev 23238
added is_atomic;
removed unused is_all;
wenzelm [Mon, 04 Jun 2007 21:04:19 +0200] rev 23237
added assume_rule_tac;
haftmann [Mon, 04 Jun 2007 15:43:32 +0200] rev 23236
reverted appnd to append
haftmann [Mon, 04 Jun 2007 15:43:31 +0200] rev 23235
authentic syntax for List.append
haftmann [Mon, 04 Jun 2007 15:43:30 +0200] rev 23234
tuned comments
urbanc [Mon, 04 Jun 2007 13:22:22 +0200] rev 23233
added a few comments to the proofs
chaieb [Mon, 04 Jun 2007 11:39:19 +0200] rev 23232
removed fixmes
chaieb [Mon, 04 Jun 2007 11:38:34 +0200] rev 23231
opaque-constraint removed
chaieb [Mon, 04 Jun 2007 09:57:02 +0200] rev 23230
tuned;
wenzelm [Sun, 03 Jun 2007 23:16:57 +0200] rev 23229
monomorphic equality: let ML work out the details;
wenzelm [Sun, 03 Jun 2007 23:16:56 +0200] rev 23228
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
wenzelm [Sun, 03 Jun 2007 23:16:55 +0200] rev 23227
tuned Tactic signature;
wenzelm [Sun, 03 Jun 2007 23:16:54 +0200] rev 23226
removed obsolete Library.seq;
wenzelm [Sun, 03 Jun 2007 23:16:53 +0200] rev 23225
moved flip to library.ML;
removed unused dest/unfold/unfold_rev;
simplified fold/fold_rev/fold_map;
wenzelm [Sun, 03 Jun 2007 23:16:52 +0200] rev 23224
added CSUBGOAL;
wenzelm [Sun, 03 Jun 2007 23:16:51 +0200] rev 23223
cleaned up signature;
wenzelm [Sun, 03 Jun 2007 23:16:50 +0200] rev 23222
added downto0 (from library.ML);
wenzelm [Sun, 03 Jun 2007 23:16:49 +0200] rev 23221
merge_ss: plain merge of prems;
wenzelm [Sun, 03 Jun 2007 23:16:48 +0200] rev 23220
added flip (from General/basics.ML);
renamed gen_submultiset to submultiset;
moved downto0 to pattern.ML;
moved legacy gen_merge_lists/merge_lists/merge_alists to Isar/locale.ML;
moved plural to HOL/Tools/fundef_lib.ML;
removed obsolete seq;
simplified chop, fold2;
wenzelm [Sun, 03 Jun 2007 23:16:47 +0200] rev 23219
tuned document;
wenzelm [Sun, 03 Jun 2007 23:16:46 +0200] rev 23218
use antiquotations instead of raw TeX code;
tuned document;
wenzelm [Sun, 03 Jun 2007 23:16:45 +0200] rev 23217
name_of_fqgar: precise type;
wenzelm [Sun, 03 Jun 2007 23:16:44 +0200] rev 23216
added plural (from Pure/library.ML);
removed unused eq_str;
wenzelm [Sun, 03 Jun 2007 23:16:43 +0200] rev 23215
local open FundefLib;
wenzelm [Sun, 03 Jun 2007 23:16:42 +0200] rev 23214
renamed gen_submultiset to submultiset;
wenzelm [Sun, 03 Jun 2007 23:16:41 +0200] rev 23213
HOL-ex: tuned deps;
nipkow [Sun, 03 Jun 2007 16:57:51 +0200] rev 23212
tuned list comprehension, added lemma
nipkow [Sun, 03 Jun 2007 15:44:35 +0200] rev 23211
fixed tex error
nipkow [Sun, 03 Jun 2007 13:19:03 +0200] rev 23210
*** empty log message ***
nipkow [Sun, 03 Jun 2007 12:58:28 +0200] rev 23209
*** empty log message ***
webertj [Sat, 02 Jun 2007 20:14:38 +0200] rev 23208
extended
webertj [Sat, 02 Jun 2007 19:10:04 +0200] rev 23207
cosmetic
wenzelm [Sat, 02 Jun 2007 18:35:38 +0200] rev 23206
made SML/NJ happy;
wenzelm [Sat, 02 Jun 2007 18:05:34 +0200] rev 23205
added target/local_abbrev (from proof_context.ML);
target_abbrev: demand equal head const (tool compliance);
wenzelm [Sat, 02 Jun 2007 18:05:33 +0200] rev 23204
moved specific target/local_abbrev to theory_target.ML;
krauss [Sat, 02 Jun 2007 15:28:38 +0200] rev 23203
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
more cleanup.
krauss [Sat, 02 Jun 2007 15:26:32 +0200] rev 23202
added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction
wenzelm [Sat, 02 Jun 2007 13:52:07 +0200] rev 23201
proper handling of Tools;
webertj [Sat, 02 Jun 2007 08:54:05 +0200] rev 23200
cosmetic
webertj [Sat, 02 Jun 2007 08:50:29 +0200] rev 23199
refute_tac made more deterministic
webertj [Sat, 02 Jun 2007 03:17:44 +0200] rev 23198
extended
webertj [Sat, 02 Jun 2007 03:15:35 +0200] rev 23197
cosmetic
webertj [Sat, 02 Jun 2007 00:09:02 +0200] rev 23196
tracing disabled
webertj [Fri, 01 Jun 2007 23:52:06 +0200] rev 23195
additional tracing information
webertj [Fri, 01 Jun 2007 23:33:49 +0200] rev 23194
tuned
webertj [Fri, 01 Jun 2007 23:21:40 +0200] rev 23193
some tests for arith added
nipkow [Fri, 01 Jun 2007 22:09:16 +0200] rev 23192
Moved list comprehension into List
webertj [Fri, 01 Jun 2007 20:34:12 +0200] rev 23191
MiniSAT mentioned in comment
webertj [Fri, 01 Jun 2007 16:04:13 +0200] rev 23190
fixed handling of meta-logic propositions
krauss [Fri, 01 Jun 2007 15:57:45 +0200] rev 23189
simplified interfaces, some restructuring
krauss [Fri, 01 Jun 2007 15:20:53 +0200] rev 23188
updated
krauss [Fri, 01 Jun 2007 15:18:31 +0200] rev 23187
added some bibtex entries
krauss [Fri, 01 Jun 2007 15:14:05 +0200] rev 23186
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss [Fri, 01 Jun 2007 15:12:56 +0200] rev 23185
Added simp-rules: "R O {} = {}" and "{} O R = {}"
haftmann [Fri, 01 Jun 2007 10:44:31 +0200] rev 23184
rudimenary
haftmann [Fri, 01 Jun 2007 10:44:30 +0200] rev 23183
tuned
haftmann [Fri, 01 Jun 2007 10:44:28 +0200] rev 23182
dropped superfluous name bindings
haftmann [Fri, 01 Jun 2007 10:44:26 +0200] rev 23181
localized
haftmann [Fri, 01 Jun 2007 10:44:24 +0200] rev 23180
fixed typo
wenzelm [Thu, 31 May 2007 23:47:38 +0200] rev 23179
insert: canonical argument order;
wenzelm [Thu, 31 May 2007 23:47:36 +0200] rev 23178
simplified/unified list fold;
huffman [Thu, 31 May 2007 23:02:16 +0200] rev 23177
replace (- 1) with -1
huffman [Thu, 31 May 2007 22:23:50 +0200] rev 23176
simplify some proofs
wenzelm [Thu, 31 May 2007 21:09:14 +0200] rev 23175
tuned headers -- adapted to usual conventions;
wenzelm [Thu, 31 May 2007 20:55:33 +0200] rev 23174
moved Compute_Oracle from Pure/Tools to Tools;
wenzelm [Thu, 31 May 2007 20:55:32 +0200] rev 23173
proper theory setup for compute oracle (based on CPure);
simplified oracle setup;
wenzelm [Thu, 31 May 2007 20:55:31 +0200] rev 23172
moved IsaPlanner from Provers to Tools;
moved Compute_Oracle from Pure/Tools to Tools;
wenzelm [Thu, 31 May 2007 20:55:29 +0200] rev 23171
moved IsaPlanner from Provers to Tools;
wenzelm [Thu, 31 May 2007 19:11:19 +0200] rev 23170
made aconvc pervasive;
wenzelm [Thu, 31 May 2007 18:31:36 +0200] rev 23169
moved aconvc to more_thm.ML;
wenzelm [Thu, 31 May 2007 18:16:59 +0200] rev 23168
tuned ML setup;
wenzelm [Thu, 31 May 2007 18:16:58 +0200] rev 23167
decode_term: force qualified name into Const;
wenzelm [Thu, 31 May 2007 18:16:57 +0200] rev 23166
proper loading of ML files (in HOL.thy);
moved Integ files to canonical place;
misc cleanup;
wenzelm [Thu, 31 May 2007 18:16:54 +0200] rev 23165
HOL_proofs;
wenzelm [Thu, 31 May 2007 18:16:52 +0200] rev 23164
moved Integ files to canonical place;
wenzelm [Thu, 31 May 2007 18:16:51 +0200] rev 23163
proper loading of ML files;
wenzelm [Thu, 31 May 2007 18:16:50 +0200] rev 23162
removed dead code;
wenzelm [Thu, 31 May 2007 18:16:47 +0200] rev 23161
tuned header;
wenzelm [Thu, 31 May 2007 18:16:46 +0200] rev 23160
doc: exclude isabelle_isar.pdf;
urbanc [Thu, 31 May 2007 15:23:35 +0200] rev 23159
tuned the proof
urbanc [Thu, 31 May 2007 14:47:20 +0200] rev 23158
introduced symmetric variants of the lemmas for alpha-equivalence
wenzelm [Thu, 31 May 2007 14:34:09 +0200] rev 23157
proper loading of ML files;
removed obsolete IFOL.thy/FOL.thy values;
wenzelm [Thu, 31 May 2007 14:34:07 +0200] rev 23156
removed obsolete IFOL.thy/FOL.thy values;
wenzelm [Thu, 31 May 2007 14:34:06 +0200] rev 23155
proper loading of ML files;
wenzelm [Thu, 31 May 2007 14:34:05 +0200] rev 23154
tuned header;
wenzelm [Thu, 31 May 2007 14:24:27 +0200] rev 23153
tuned oracle setup;
wenzelm [Thu, 31 May 2007 14:01:58 +0200] rev 23152
moved HOLCF tools to canonical place;
wenzelm [Thu, 31 May 2007 13:24:13 +0200] rev 23151
moved TFL files to canonical place;
wenzelm [Thu, 31 May 2007 13:18:52 +0200] rev 23150
moved TFL files to canonical place;
wenzelm [Thu, 31 May 2007 13:18:42 +0200] rev 23149
added src/Tools;
moved TFL files to canonical place;
wenzelm [Thu, 31 May 2007 13:00:56 +0200] rev 23148
fixed title;
wenzelm [Thu, 31 May 2007 12:59:31 +0200] rev 23147
Tools: generic tools outside of Pure.
wenzelm [Thu, 31 May 2007 12:06:31 +0200] rev 23146
moved Integ files to canonical place;
wenzelm [Thu, 31 May 2007 11:00:06 +0200] rev 23145
fixed use_thy "LocalWeakening";
urbanc [Thu, 31 May 2007 10:17:23 +0200] rev 23144
included new example in the compiling process
urbanc [Thu, 31 May 2007 09:48:20 +0200] rev 23143
a theory using locally nameless terms and strong induction principles
urbanc [Thu, 31 May 2007 09:14:14 +0200] rev 23142
tuned the proof
wenzelm [Thu, 31 May 2007 01:36:08 +0200] rev 23141
emulate later version of TextIO.inputLine;
wenzelm [Thu, 31 May 2007 01:25:35 +0200] rev 23140
reversed SML B library patches;
wenzelm [Thu, 31 May 2007 01:25:24 +0200] rev 23139
TextIO.inputLine: use present SML B library version;
wenzelm [Wed, 30 May 2007 23:32:54 +0200] rev 23138
tuned USEDIR_OPTIONS;
PDF_VIEWER: try to be smart for MacOS (Darwin);
wenzelm [Wed, 30 May 2007 23:31:57 +0200] rev 23137
removed HOL4 image, which seldom works;
haftmann [Wed, 30 May 2007 21:09:18 +0200] rev 23136
simplified data setup
haftmann [Wed, 30 May 2007 21:09:17 +0200] rev 23135
instance: always print sorts on failure
haftmann [Wed, 30 May 2007 21:09:16 +0200] rev 23134
more example
haftmann [Wed, 30 May 2007 21:09:15 +0200] rev 23133
fixed typo
haftmann [Wed, 30 May 2007 21:09:13 +0200] rev 23132
updated
haftmann [Wed, 30 May 2007 21:09:12 +0200] rev 23131
generalized lemmas
haftmann [Wed, 30 May 2007 21:09:11 +0200] rev 23130
eliminated strings
haftmann [Wed, 30 May 2007 21:09:09 +0200] rev 23129
tuned
krauss [Wed, 30 May 2007 18:05:10 +0200] rev 23128
clarified error message
huffman [Wed, 30 May 2007 02:41:26 +0200] rev 23127
simplify names of locale interpretations
huffman [Wed, 30 May 2007 01:53:38 +0200] rev 23126
renamed some lemmas in Complex.thy
huffman [Wed, 30 May 2007 01:46:05 +0200] rev 23125
cleaned up proofs; reorganized sections; removed redundant lemmas
huffman [Tue, 29 May 2007 20:53:13 +0200] rev 23124
use new-style instance declarations
huffman [Tue, 29 May 2007 20:31:53 +0200] rev 23123
instance complex :: banach
huffman [Tue, 29 May 2007 20:31:42 +0200] rev 23122
add lemma real_sqrt_sum_squares_less
huffman [Tue, 29 May 2007 18:31:30 +0200] rev 23121
cleaned up some proofs
huffman [Tue, 29 May 2007 18:19:56 +0200] rev 23120
interpretation bounded_linear_divide
huffman [Tue, 29 May 2007 17:37:04 +0200] rev 23119
add bounded_linear lemmas
huffman [Tue, 29 May 2007 17:36:35 +0200] rev 23118
add isUCont lemmas
krauss [Tue, 29 May 2007 14:03:49 +0200] rev 23117
updated examples to include an instance of (lexicographic_order simp:...)
huffman [Mon, 28 May 2007 16:30:28 +0200] rev 23116
Complex: generalized type of exp
huffman [Mon, 28 May 2007 16:29:17 +0200] rev 23115
generalized exp to work over any complete field; new proof of exp_add
huffman [Mon, 28 May 2007 16:27:33 +0200] rev 23114
add type annotations for exp
huffman [Mon, 28 May 2007 04:22:44 +0200] rev 23113
interpretations additive_scaleR_left, additive_scaleR_right
huffman [Mon, 28 May 2007 03:45:41 +0200] rev 23112
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman [Sun, 27 May 2007 20:04:02 +0200] rev 23111
new proof of Cauchy product formula for series
nipkow [Sat, 26 May 2007 07:26:03 +0200] rev 23110
What it says
haftmann [Fri, 25 May 2007 21:08:53 +0200] rev 23109
improved error handling
haftmann [Fri, 25 May 2007 21:08:52 +0200] rev 23108
using rudimentary class target mechanism
haftmann [Fri, 25 May 2007 21:08:46 +0200] rev 23107
*** empty log message ***
haftmann [Fri, 25 May 2007 21:08:45 +0200] rev 23106
fixed typo
huffman [Fri, 25 May 2007 18:25:17 +0200] rev 23105
fix typos
nipkow [Fri, 25 May 2007 18:24:11 +0200] rev 23104
*** empty log message ***
nipkow [Fri, 25 May 2007 18:11:25 +0200] rev 23103
*** empty log message ***
nipkow [Fri, 25 May 2007 18:10:56 +0200] rev 23102
*** empty log message ***
nipkow [Fri, 25 May 2007 18:08:47 +0200] rev 23101
tuned
nipkow [Fri, 25 May 2007 18:08:34 +0200] rev 23100
Added List_Comprehension
urbanc [Fri, 25 May 2007 06:06:49 +0200] rev 23099
adapted to fix for fresh_fun_simp
urbanc [Fri, 25 May 2007 05:18:56 +0200] rev 23098
took out Class.thy from the compiling process until memory problems are solved
huffman [Fri, 25 May 2007 00:36:54 +0200] rev 23097
simplify some proofs
nipkow [Thu, 24 May 2007 22:55:53 +0200] rev 23096
*** empty log message ***
obua [Thu, 24 May 2007 16:52:54 +0200] rev 23095
Squared things out.
narboux [Thu, 24 May 2007 14:04:06 +0200] rev 23094
fix a bug : the semantics of no_asm was the opposite
urbanc [Thu, 24 May 2007 13:59:54 +0200] rev 23093
temporary fix for a bug in fresh_fun_simp
urbanc [Thu, 24 May 2007 12:09:38 +0200] rev 23092
formalisation of my PhD (the result was correct, but the proof needed several corrections)
narboux [Thu, 24 May 2007 12:00:47 +0200] rev 23091
add an option in fresh_fun_simp to prevent rewriting in assumptions
haftmann [Thu, 24 May 2007 08:37:43 +0200] rev 23090
fixes tvar issue in type inference
haftmann [Thu, 24 May 2007 08:37:42 +0200] rev 23089
tuned
haftmann [Thu, 24 May 2007 08:37:41 +0200] rev 23088
tuned warning
haftmann [Thu, 24 May 2007 08:37:39 +0200] rev 23087
rudimentary class target implementation
haftmann [Thu, 24 May 2007 08:37:37 +0200] rev 23086
tuned Pure/General/name_space.ML
nipkow [Thu, 24 May 2007 07:27:44 +0200] rev 23085
Introduced new classes monoid_add and group_add
huffman [Wed, 23 May 2007 19:23:22 +0200] rev 23084
add lemma complete_algebra_summable_geometric
paulson [Wed, 23 May 2007 14:52:12 +0200] rev 23083
formatting
huffman [Wed, 23 May 2007 07:00:18 +0200] rev 23082
generalize powerseries and termdiffs lemmas using axclasses
huffman [Wed, 23 May 2007 02:50:19 +0200] rev 23081
remove unused simproc definition
huffman [Wed, 23 May 2007 02:33:42 +0200] rev 23080
remove redundant simproc; remove legacy ML bindings
huffman [Wed, 23 May 2007 01:46:15 +0200] rev 23079
remove redundant simproc
huffman [Tue, 22 May 2007 21:32:04 +0200] rev 23078
new simp rule Infinitesimal_of_hypreal_iff
huffman [Tue, 22 May 2007 19:58:54 +0200] rev 23077
removed redundant lemmas
huffman [Tue, 22 May 2007 19:47:55 +0200] rev 23076
generalize uniqueness of limits to class real_normed_algebra_1
paulson [Tue, 22 May 2007 17:56:06 +0200] rev 23075
Some hacks for SPASS format
krauss [Tue, 22 May 2007 17:25:26 +0200] rev 23074
some optimizations, cleanup
huffman [Tue, 22 May 2007 16:47:22 +0200] rev 23073
add missing instance declarations
haftmann [Tue, 22 May 2007 14:43:54 +0200] rev 23072
adjusted to change in Provers/Arith/combine_numerals.ML
haftmann [Tue, 22 May 2007 13:55:30 +0200] rev 23071
adjusted to change in Provers/Arith/combine_numerals.ML
krauss [Tue, 22 May 2007 13:40:37 +0200] rev 23070
regression tests: send failure reports to krauss@in.tum.de, too
huffman [Tue, 22 May 2007 07:29:49 +0200] rev 23069
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman [Tue, 22 May 2007 05:07:48 +0200] rev 23068
remove obsolete CSeries.thy
huffman [Tue, 22 May 2007 00:38:51 +0200] rev 23067
generalized ring_eq_cancel simprocs to class idom; removed redundant field_eq_cancel simprocs
huffman [Mon, 21 May 2007 19:43:33 +0200] rev 23066
new field_combine_numerals simproc, which uses fractions as coefficients
narboux [Mon, 21 May 2007 19:14:12 +0200] rev 23065
search bottom up to get the inner fresh fun
narboux [Mon, 21 May 2007 19:13:38 +0200] rev 23064
add a bottom up search function
haftmann [Mon, 21 May 2007 19:11:42 +0200] rev 23063
tuned
haftmann [Mon, 21 May 2007 19:11:41 +0200] rev 23062
evaluation for integers
haftmann [Mon, 21 May 2007 19:11:40 +0200] rev 23061
added lemma divAlg_div_mof
haftmann [Mon, 21 May 2007 19:11:39 +0200] rev 23060
improved code for rev
haftmann [Mon, 21 May 2007 19:11:38 +0200] rev 23059
min/max
huffman [Mon, 21 May 2007 19:05:37 +0200] rev 23058
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman [Mon, 21 May 2007 18:53:04 +0200] rev 23057
add lemmas divide_numeral_1 and inverse_numeral_1
krauss [Mon, 21 May 2007 16:39:58 +0200] rev 23056
fixed signature
krauss [Mon, 21 May 2007 16:22:46 +0200] rev 23055
Method "lexicographic_order" now takes the same arguments as "auto"
narboux [Mon, 21 May 2007 16:19:56 +0200] rev 23054
change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
huffman [Sun, 20 May 2007 18:48:52 +0200] rev 23053
define pi with THE instead of SOME; cleaned up
huffman [Sun, 20 May 2007 17:49:10 +0200] rev 23052
add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
huffman [Sun, 20 May 2007 17:30:21 +0200] rev 23051
add lemma power2_eq_imp_eq
urbanc [Sun, 20 May 2007 13:39:46 +0200] rev 23050
added lemma for permutations on strings
huffman [Sun, 20 May 2007 10:13:06 +0200] rev 23049
moved sqrt lemmas from Transcendental.thy to NthRoot.thy
huffman [Sun, 20 May 2007 09:50:56 +0200] rev 23048
remove obsolete DERIV_ln lemmas
huffman [Sun, 20 May 2007 09:21:04 +0200] rev 23047
add realpow_pos_nth2 back in
huffman [Sun, 20 May 2007 09:05:44 +0200] rev 23046
add odd_real_root lemmas
huffman [Sun, 20 May 2007 08:16:29 +0200] rev 23045
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman [Sun, 20 May 2007 08:00:48 +0200] rev 23044
change premises of DERIV_inverse_function lemma
huffman [Sun, 20 May 2007 05:27:45 +0200] rev 23043
rearranged sections
huffman [Sun, 20 May 2007 03:19:42 +0200] rev 23042
add lemmas about continuity and derivatives of roots
huffman [Sun, 20 May 2007 03:19:14 +0200] rev 23041
add lemma DERIV_inverse_function
huffman [Sun, 20 May 2007 03:18:50 +0200] rev 23040
add lemmas LIM_compose2, isCont_LIM_compose2
haftmann [Sat, 19 May 2007 19:35:31 +0200] rev 23039
improved aliassing
haftmann [Sat, 19 May 2007 19:35:17 +0200] rev 23038
more robust thm handling
chaieb [Sat, 19 May 2007 19:08:42 +0200] rev 23037
added a set of NNF normalization lemmas and nnf_conv
chaieb [Sat, 19 May 2007 19:08:06 +0200] rev 23036
added lt and some other infix operation analogous to Ocaml's num library
chaieb [Sat, 19 May 2007 18:20:34 +0200] rev 23035
added a generic conversion for quantifier elimination and a special useful instance
chaieb [Sat, 19 May 2007 18:19:45 +0200] rev 23034
added binop_conv, aconvc
chaieb [Sat, 19 May 2007 18:19:06 +0200] rev 23033
added cpat antiquotation for reading certified patterns
nipkow [Sat, 19 May 2007 14:05:05 +0200] rev 23032
unfold min/max in Stefans code generator
nipkow [Sat, 19 May 2007 13:41:13 +0200] rev 23031
added code generation based on Isabelle's rat type.
nipkow [Sat, 19 May 2007 13:40:33 +0200] rev 23030
Disabled Stefancs code generator - already enabled in RealDef.
haftmann [Sat, 19 May 2007 11:33:57 +0200] rev 23029
constant op @ now named append
haftmann [Sat, 19 May 2007 11:33:34 +0200] rev 23028
fixed comment
haftmann [Sat, 19 May 2007 11:33:33 +0200] rev 23027
dropped legacy
haftmann [Sat, 19 May 2007 11:33:32 +0200] rev 23026
improved eta expansion
haftmann [Sat, 19 May 2007 11:33:31 +0200] rev 23025
dropped nonsense comment
haftmann [Sat, 19 May 2007 11:33:30 +0200] rev 23024
fixed text
haftmann [Sat, 19 May 2007 11:33:28 +0200] rev 23023
eliminated name clash with List.append
haftmann [Sat, 19 May 2007 11:33:26 +0200] rev 23022
added qualification for ambiguous definition names
haftmann [Sat, 19 May 2007 11:33:25 +0200] rev 23021
tuned
haftmann [Sat, 19 May 2007 11:33:24 +0200] rev 23020
typ_of instance for int
haftmann [Sat, 19 May 2007 11:33:23 +0200] rev 23019
hide locale predicate "field" from HOL library
haftmann [Sat, 19 May 2007 11:33:22 +0200] rev 23018
no special treatment in naming of locale predicates stemming form classes
haftmann [Sat, 19 May 2007 11:33:21 +0200] rev 23017
uniform module names for code generation
haftmann [Sat, 19 May 2007 11:33:20 +0200] rev 23016
added Executable_Real
haftmann [Sat, 19 May 2007 11:33:19 +0200] rev 23015
updated
nipkow [Sat, 19 May 2007 08:43:15 +0200] rev 23014
Had to replace "case 1/2" by "case base/step". No idea why.
nipkow [Sat, 19 May 2007 07:47:51 +0200] rev 23013
*** empty log message ***
huffman [Sat, 19 May 2007 04:52:24 +0200] rev 23012
remove dependence on Hilbert_Choice.thy
huffman [Sat, 19 May 2007 04:51:03 +0200] rev 23011
use THE instead of SOME
huffman [Fri, 18 May 2007 18:20:39 +0200] rev 23010
minimize imports
huffman [Fri, 18 May 2007 17:35:07 +0200] rev 23009
Prove existence of nth roots using Intermediate Value Theorem
huffman [Fri, 18 May 2007 16:13:07 +0200] rev 23008
avoid using real_mult_inverse_left; cleaned up
huffman [Fri, 18 May 2007 16:11:13 +0200] rev 23007
use mult_strict_mono instead of real_mult_less_mono
berghofe [Fri, 18 May 2007 11:12:03 +0200] rev 23006
Fixed bug in subst causing primrec functions returning functions
to be rejected.
haftmann [Fri, 18 May 2007 09:16:57 +0200] rev 23005
dropped word_setup.ML
krauss [Thu, 17 May 2007 23:04:54 +0200] rev 23004
added files
krauss [Thu, 17 May 2007 23:03:47 +0200] rev 23003
updated
krauss [Thu, 17 May 2007 23:00:06 +0200] rev 23002
moved lemmas to Nat.thy
krauss [Thu, 17 May 2007 22:58:53 +0200] rev 23001
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss [Thu, 17 May 2007 22:37:34 +0200] rev 23000
added pointer to new Unification theory
krauss [Thu, 17 May 2007 22:33:41 +0200] rev 22999
Added unification case study (using new function package)
huffman [Thu, 17 May 2007 21:51:32 +0200] rev 22998
avoid using redundant lemmas from RealDef.thy
haftmann [Thu, 17 May 2007 19:49:40 +0200] rev 22997
canonical prefixing of class constants
haftmann [Thu, 17 May 2007 19:49:21 +0200] rev 22996
dropped beta/eta normalization of defining equations
haftmann [Thu, 17 May 2007 19:49:20 +0200] rev 22995
refined pow function
haftmann [Thu, 17 May 2007 19:49:17 +0200] rev 22994
abstract size function in hologic.ML
haftmann [Thu, 17 May 2007 19:49:16 +0200] rev 22993
tuned
huffman [Thu, 17 May 2007 19:29:39 +0200] rev 22992
add classes ring_no_zero_divisors and dom
huffman [Thu, 17 May 2007 19:12:47 +0200] rev 22991
generalize class restrictions on some lemmas
huffman [Thu, 17 May 2007 18:32:17 +0200] rev 22990
added classes ring_no_zero_divisors and dom (non-commutative version of idom);
generalized several cancellation lemmas to use the new classes
paulson [Thu, 17 May 2007 13:37:24 +0200] rev 22989
Added three items to the signature
huffman [Thu, 17 May 2007 08:53:57 +0200] rev 22988
generalize some lemmas from field to division_ring
huffman [Thu, 17 May 2007 08:42:51 +0200] rev 22987
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman [Thu, 17 May 2007 08:41:23 +0200] rev 22986
remove redundant instance declaration
huffman [Thu, 17 May 2007 00:45:27 +0200] rev 22985
cleaned up proof of Maclaurin_sin_bound
huffman [Wed, 16 May 2007 23:07:08 +0200] rev 22984
section labels
huffman [Wed, 16 May 2007 23:03:45 +0200] rev 22983
minimize imports
chaieb [Wed, 16 May 2007 09:45:22 +0200] rev 22982
dropped |R
chaieb [Tue, 15 May 2007 18:28:02 +0200] rev 22981
A verified theory for rational numbers representation and simple calculations;
verified with respect to the real numbers;
berghofe [Tue, 15 May 2007 18:20:07 +0200] rev 22980
Fixed bug that caused proof of induction theorem to fail if
introduction rules contained True or False.
huffman [Tue, 15 May 2007 08:10:31 +0200] rev 22979
minimize imports
huffman [Tue, 15 May 2007 07:28:08 +0200] rev 22978
clean up polar_Ex proofs; remove unnecessary lemmas
huffman [Tue, 15 May 2007 05:09:01 +0200] rev 22977
remove simp attribute from various polar_Ex lemmas
huffman [Mon, 14 May 2007 23:25:16 +0200] rev 22976
tuned proofs
huffman [Mon, 14 May 2007 23:09:54 +0200] rev 22975
spelling: rename arcos -> arccos
huffman [Mon, 14 May 2007 22:32:51 +0200] rev 22974
tuned proofs
huffman [Mon, 14 May 2007 20:48:32 +0200] rev 22973
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman [Mon, 14 May 2007 20:14:31 +0200] rev 22972
generalized sgn function to work on any real normed vector space
huffman [Mon, 14 May 2007 19:14:50 +0200] rev 22971
root and sqrt on negative inputs
huffman [Mon, 14 May 2007 18:48:24 +0200] rev 22970
move lemmas to RealPow.thy; tuned proofs
huffman [Mon, 14 May 2007 18:04:52 +0200] rev 22969
tuned proofs
huffman [Mon, 14 May 2007 18:03:25 +0200] rev 22968
tuned
huffman [Mon, 14 May 2007 17:45:42 +0200] rev 22967
added general sum-squares lemmas
huffman [Mon, 14 May 2007 17:37:31 +0200] rev 22966
new lemmas
webertj [Mon, 14 May 2007 13:24:22 +0200] rev 22965
ProofGeneral: Find Theorems search form
haftmann [Mon, 14 May 2007 12:52:56 +0200] rev 22964
reorganized float arithmetic
haftmann [Mon, 14 May 2007 12:52:54 +0200] rev 22963
fixed IntInf ambiguity
huffman [Mon, 14 May 2007 09:33:18 +0200] rev 22962
remove redundant lemmas
huffman [Mon, 14 May 2007 09:27:24 +0200] rev 22961
remove redundant lemmas
huffman [Mon, 14 May 2007 09:16:47 +0200] rev 22960
remove redundant lemmas
huffman [Mon, 14 May 2007 09:11:30 +0200] rev 22959
remove redundant lemmas
huffman [Mon, 14 May 2007 08:15:13 +0200] rev 22958
cleaned up
huffman [Mon, 14 May 2007 08:12:38 +0200] rev 22957
tuned
huffman [Sun, 13 May 2007 20:05:42 +0200] rev 22956
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
huffman [Sun, 13 May 2007 19:15:36 +0200] rev 22955
add lemma power_eq_imp_eq_base
haftmann [Sun, 13 May 2007 18:16:49 +0200] rev 22954
added module int
haftmann [Sun, 13 May 2007 18:15:30 +0200] rev 22953
dropped legacy
haftmann [Sun, 13 May 2007 18:15:28 +0200] rev 22952
removed module rat.ML
haftmann [Sun, 13 May 2007 18:15:26 +0200] rev 22951
whitespace tuned
haftmann [Sun, 13 May 2007 18:15:25 +0200] rev 22950
tuned
haftmann [Sun, 13 May 2007 18:15:24 +0200] rev 22949
fixed omission
haftmann [Sun, 13 May 2007 18:15:23 +0200] rev 22948
tuned setup
haftmann [Sun, 13 May 2007 18:15:22 +0200] rev 22947
refined module rat
haftmann [Sun, 13 May 2007 18:15:21 +0200] rev 22946
added modules rat.ML and int.ML
nipkow [Sun, 13 May 2007 09:23:27 +0200] rev 22945
Removed junk
nipkow [Sun, 13 May 2007 07:11:21 +0200] rev 22944
Got rid of listsp
huffman [Sun, 13 May 2007 04:38:24 +0200] rev 22943
removed redundant lemmas
huffman [Sat, 12 May 2007 18:16:30 +0200] rev 22942
add lemma additive.setsum
nipkow [Fri, 11 May 2007 20:47:30 +0200] rev 22941
*** empty log message ***
nipkow [Fri, 11 May 2007 20:07:00 +0200] rev 22940
*** empty log message ***
wenzelm [Fri, 11 May 2007 18:49:15 +0200] rev 22939
proper type for fun/arg_cong_rule;
wenzelm [Fri, 11 May 2007 18:47:08 +0200] rev 22938
added fun/arg_cong_rule;
wenzelm [Fri, 11 May 2007 18:46:50 +0200] rev 22937
unified names: foo_conv;
wenzelm [Fri, 11 May 2007 17:54:36 +0200] rev 22936
tuned;
krauss [Fri, 11 May 2007 15:37:42 +0200] rev 22935
added fun flip f x y = f y x
huffman [Fri, 11 May 2007 03:31:12 +0200] rev 22934
generalize setsum lemmas from semiring_0_cancel to semiring_0
wenzelm [Fri, 11 May 2007 01:07:10 +0200] rev 22933
tuned proofs;
wenzelm [Fri, 11 May 2007 00:43:46 +0200] rev 22932
bang_facts: warning;
wenzelm [Fri, 11 May 2007 00:43:45 +0200] rev 22931
tuned proofs;
haftmann [Thu, 10 May 2007 22:11:38 +0200] rev 22930
(class target)
haftmann [Thu, 10 May 2007 22:11:37 +0200] rev 22929
cleaned up
haftmann [Thu, 10 May 2007 22:11:36 +0200] rev 22928
beta/eta conversion after preprocessor
haftmann [Thu, 10 May 2007 22:11:35 +0200] rev 22927
fixed typo
wenzelm [Thu, 10 May 2007 18:10:32 +0200] rev 22926
more conversions;
tuned;
berghofe [Thu, 10 May 2007 15:51:59 +0200] rev 22925
Moved extraction_expand declaration of listall_def outside of definition.
berghofe [Thu, 10 May 2007 15:50:56 +0200] rev 22924
Adapted to new naming scheme for definitions.
berghofe [Thu, 10 May 2007 15:50:28 +0200] rev 22923
Changed name of raw definition.
berghofe [Thu, 10 May 2007 15:49:31 +0200] rev 22922
Name of ML function "not" is now qualified in order to avoid
clashes with names of constants introduced by the user.
haftmann [Thu, 10 May 2007 10:22:17 +0200] rev 22921
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann [Thu, 10 May 2007 10:21:50 +0200] rev 22920
size [nat] is identity
haftmann [Thu, 10 May 2007 10:21:48 +0200] rev 22919
explicit import of Datatype.thy due to hook bootstrap problem
haftmann [Thu, 10 May 2007 10:21:47 +0200] rev 22918
localized Sup/Inf
haftmann [Thu, 10 May 2007 10:21:46 +0200] rev 22917
localized Min/Max
haftmann [Thu, 10 May 2007 10:21:44 +0200] rev 22916
tuned
huffman [Thu, 10 May 2007 04:06:56 +0200] rev 22915
fix proofs
huffman [Thu, 10 May 2007 03:11:03 +0200] rev 22914
remove redundant lemmas
huffman [Thu, 10 May 2007 03:07:26 +0200] rev 22913
lemmas iszero_(h)complex_number_of are no longer needed
huffman [Thu, 10 May 2007 03:00:15 +0200] rev 22912
instance real_algebra_1 < ring_char_0
huffman [Thu, 10 May 2007 02:51:53 +0200] rev 22911
new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
wenzelm [Thu, 10 May 2007 00:39:56 +0200] rev 22910
moved conversions to structure Conv;
get_axiom_i;
wenzelm [Thu, 10 May 2007 00:39:55 +0200] rev 22909
added dest_fun/fun2/arg1;
removed dest_binop;
renamed cterm_(fo_)match to (fo_)match;
renamed cterm_incr_indexes to incr_indexes_cterm;
wenzelm [Thu, 10 May 2007 00:39:54 +0200] rev 22908
tuned argument_type_of;
wenzelm [Thu, 10 May 2007 00:39:53 +0200] rev 22907
added destructors from drule.ML;
added mk_binop;
wenzelm [Thu, 10 May 2007 00:39:52 +0200] rev 22906
moved some operations to more_thm.ML and conv.ML;
wenzelm [Thu, 10 May 2007 00:39:51 +0200] rev 22905
Conversions: primitive equality reasoning (from drule.ML);
wenzelm [Thu, 10 May 2007 00:39:50 +0200] rev 22904
added conv.ML;
wenzelm [Thu, 10 May 2007 00:39:49 +0200] rev 22903
Thm.match;
wenzelm [Thu, 10 May 2007 00:39:48 +0200] rev 22902
moved some Drule operations to Thm (see more_thm.ML);
wenzelm [Thu, 10 May 2007 00:39:46 +0200] rev 22901
Thm.first_order_match;
wenzelm [Thu, 10 May 2007 00:39:45 +0200] rev 22900
moved conversions to structure Conv;
krauss [Wed, 09 May 2007 23:28:18 +0200] rev 22899
"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"
huffman [Wed, 09 May 2007 22:14:26 +0200] rev 22898
add lemma norm_diff_ineq; shorten other proofs
wenzelm [Wed, 09 May 2007 19:37:22 +0200] rev 22897
removed Complex/ComplexBin.thy;
wenzelm [Wed, 09 May 2007 19:37:21 +0200] rev 22896
tuned ML setup;
wenzelm [Wed, 09 May 2007 19:37:20 +0200] rev 22895
tuned syntax;
wenzelm [Wed, 09 May 2007 19:37:19 +0200] rev 22894
eliminated unnamed infixes;
wenzelm [Wed, 09 May 2007 19:37:18 +0200] rev 22893
removed unused mk_cond_defpair;
wenzelm [Wed, 09 May 2007 19:20:00 +0200] rev 22892
simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification);
trace_simp_depth_limit_exceeded: attempt to hide destructive pointer programming within simpset;
huffman [Wed, 09 May 2007 18:58:03 +0200] rev 22891
remove empty, unused theory
huffman [Wed, 09 May 2007 18:26:40 +0200] rev 22890
remove redundant lemmas
huffman [Wed, 09 May 2007 18:25:44 +0200] rev 22889
add lemma hnorm_hyperpow
huffman [Wed, 09 May 2007 18:25:21 +0200] rev 22888
add lemma of_hypreal_hyperpow
haftmann [Wed, 09 May 2007 07:53:08 +0200] rev 22887
tuned
haftmann [Wed, 09 May 2007 07:53:06 +0200] rev 22886
moved recfun_codegen.ML to Code_Generator.thy
haftmann [Wed, 09 May 2007 07:53:04 +0200] rev 22885
continued
huffman [Wed, 09 May 2007 01:56:59 +0200] rev 22884
remove redundant lemmas
huffman [Wed, 09 May 2007 01:26:04 +0200] rev 22883
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman [Wed, 09 May 2007 00:57:46 +0200] rev 22882
add lemma hnorm_divide
huffman [Wed, 09 May 2007 00:33:12 +0200] rev 22881
add lemmas abs_hnorm_cancel, hnorm_of_hypreal
huffman [Wed, 09 May 2007 00:27:36 +0200] rev 22880
add lemmas norm_add_less, norm_mult_less
huffman [Tue, 08 May 2007 23:52:15 +0200] rev 22879
add lemma Standard_hyperpow
wenzelm [Tue, 08 May 2007 21:02:26 +0200] rev 22878
tuned;
huffman [Tue, 08 May 2007 19:15:35 +0200] rev 22877
add of_hypreal constant with lemmas
huffman [Tue, 08 May 2007 18:23:37 +0200] rev 22876
add lemmas norm_number_of, norm_of_int, norm_of_nat
wenzelm [Tue, 08 May 2007 17:41:35 +0200] rev 22875
quoted 'declaration';
wenzelm [Tue, 08 May 2007 17:40:22 +0200] rev 22874
simplified pretty_thm(_legacy);
wenzelm [Tue, 08 May 2007 17:40:21 +0200] rev 22873
is_sid: include '::';
wenzelm [Tue, 08 May 2007 17:40:20 +0200] rev 22872
tuned ProofDisplay.pretty_full_theory;
wenzelm [Tue, 08 May 2007 17:40:18 +0200] rev 22871
tuned;
wenzelm [Tue, 08 May 2007 15:37:27 +0200] rev 22870
updated;
wenzelm [Tue, 08 May 2007 15:37:19 +0200] rev 22869
simplified context data;