| Sat, 07 Jul 2007 00:15:02 +0200 |
wenzelm |
moved General/xml.ML to Tools/xml.ML;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:15:00 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:14:59 +0200 |
wenzelm |
simplified output mode setup;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:14:58 +0200 |
wenzelm |
added print_mode setup: indent and markup;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:14:57 +0200 |
wenzelm |
renamed raw to escape;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:14:56 +0200 |
wenzelm |
simplified pretty token metric: type int;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:14:54 +0200 |
wenzelm |
moved General/xml.ML to Tools/xml.ML;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:14:52 +0200 |
wenzelm |
added General/markup.ML;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:14:49 +0200 |
wenzelm |
added class skolem, command;
|
changeset |
files
|
| Fri, 06 Jul 2007 23:26:13 +0200 |
nipkow |
more interpretations
|
changeset |
files
|
| Fri, 06 Jul 2007 17:52:52 +0200 |
aspinall |
Produce good PGML 2.0
|
changeset |
files
|
| Fri, 06 Jul 2007 17:21:18 +0200 |
webertj |
cosmetic (line length fixed)
|
changeset |
files
|
| Fri, 06 Jul 2007 16:09:28 +0200 |
chaieb |
Some examples for reifying type variables
|
changeset |
files
|
| Fri, 06 Jul 2007 16:09:27 +0200 |
chaieb |
Tuned document
|
changeset |
files
|
| Fri, 06 Jul 2007 16:09:26 +0200 |
chaieb |
Cleaned add and del attributes
|
changeset |
files
|
| Fri, 06 Jul 2007 16:09:25 +0200 |
chaieb |
Reification now deals with type variables
|
changeset |
files
|
| Fri, 06 Jul 2007 11:55:05 +0200 |
wenzelm |
Cumulative reports for Poly/ML profiling output.
|
changeset |
files
|
| Thu, 05 Jul 2007 20:36:48 +0200 |
aspinall |
Update PGML version, add system name
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:39 +0200 |
wenzelm |
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:38 +0200 |
wenzelm |
added type conv;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:37 +0200 |
wenzelm |
removed comments -- no exception TERM;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:36 +0200 |
wenzelm |
added is_reflexive;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:34 +0200 |
wenzelm |
simplified has_meta_prems;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:33 +0200 |
wenzelm |
moved type conv to thm.ML;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:32 +0200 |
wenzelm |
the_theory/proof: error instead of exception Fail;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:31 +0200 |
wenzelm |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:30 +0200 |
wenzelm |
renamed Conv.is_refl to Thm.is_reflexive;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:29 +0200 |
wenzelm |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:28 +0200 |
wenzelm |
simplified ObjectLogic.atomize;
|
changeset |
files
|
| Thu, 05 Jul 2007 20:01:26 +0200 |
wenzelm |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
changeset |
files
|
| Thu, 05 Jul 2007 19:59:01 +0200 |
aspinall |
Revert body of pgml to match schema for now [change bad for Broker]
|
changeset |
files
|
| Thu, 05 Jul 2007 19:57:19 +0200 |
aspinall |
Classify -- comments as ordinary comments (no undo)
|
changeset |
files
|
| Thu, 05 Jul 2007 00:15:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:25 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:24 +0200 |
wenzelm |
sort_le: tuned eq case;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:23 +0200 |
wenzelm |
tuned goal conversion interfaces;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:22 +0200 |
wenzelm |
else_conv: only handle THM | CTERM | TERM | TYPE;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:20 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:19 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:18 +0200 |
wenzelm |
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:17 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:16 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:14 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:13 +0200 |
wenzelm |
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:12 +0200 |
wenzelm |
Logical operations on numerals (see also HOL/hologic.ML).
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:11 +0200 |
wenzelm |
added Tools/numeral.ML;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:10 +0200 |
wenzelm |
common normalizer_funs, avoid cterm_of;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:09 +0200 |
wenzelm |
Numeral.mk_cnumber;
|
changeset |
files
|
| Wed, 04 Jul 2007 21:20:23 +0200 |
aspinall |
PGML abstraction, draft version
|
changeset |
files
|
| Wed, 04 Jul 2007 21:19:34 +0200 |
aspinall |
Use pgml
|
changeset |
files
|
| Wed, 04 Jul 2007 17:21:02 +0200 |
obua |
fixed argument order in calls to Integer.pow
|
changeset |
files
|
| Wed, 04 Jul 2007 16:49:36 +0200 |
wenzelm |
added binop_cong_rule;
|
changeset |
files
|
| Wed, 04 Jul 2007 16:49:35 +0200 |
wenzelm |
export dlo_conv;
|
changeset |
files
|
| Wed, 04 Jul 2007 16:49:34 +0200 |
wenzelm |
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
|
changeset |
files
|
| Wed, 04 Jul 2007 14:21:00 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 04 Jul 2007 14:10:01 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 04 Jul 2007 13:56:26 +0200 |
paulson |
simplified a proof
|
changeset |
files
|
| Tue, 03 Jul 2007 23:00:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:30 +0200 |
wenzelm |
CONVERSION: handle TYPE | TERM | CTERM | THM;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:27 +0200 |
wenzelm |
proper use of ioa_package.ML;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:19 +0200 |
wenzelm |
tuned is_comb/is_binop -- avoid construction of cterms;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:16 +0200 |
wenzelm |
HOLogic.conj_intr/elims;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:13 +0200 |
wenzelm |
use mucke_oracle.ML only once;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:11 +0200 |
wenzelm |
assume basic HOL context for compilation (antiquotations);
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:08 +0200 |
wenzelm |
proper use of function_package ML files;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:05 +0200 |
wenzelm |
use hologic.ML in basic HOL context;
|
changeset |
files
|
| Tue, 03 Jul 2007 21:56:25 +0200 |
paulson |
to handle non-atomic assumptions
|
changeset |
files
|
| Tue, 03 Jul 2007 20:26:08 +0200 |
wenzelm |
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
|
changeset |
files
|
| Tue, 03 Jul 2007 18:42:09 +0200 |
huffman |
convert instance proofs to Isar style
|
changeset |
files
|
| Tue, 03 Jul 2007 18:00:57 +0200 |
chaieb |
Dependency on reflection_data.ML to build HOL-ex
|
changeset |
files
|
| Tue, 03 Jul 2007 17:50:00 +0200 |
chaieb |
Generalized case for atoms. Selection of environment lists is allowed more than once.
|
changeset |
files
|
| Tue, 03 Jul 2007 17:49:58 +0200 |
chaieb |
More examples
|
changeset |
files
|
| Tue, 03 Jul 2007 17:49:55 +0200 |
chaieb |
reflection and reification methods now manage Context data
|
changeset |
files
|
| Tue, 03 Jul 2007 17:49:53 +0200 |
chaieb |
Context Data for the reflection and reification methods
|
changeset |
files
|
| Tue, 03 Jul 2007 17:28:36 +0200 |
huffman |
rename class dom to ring_1_no_zero_divisors
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:17 +0200 |
wenzelm |
rewrite_goal_tac;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:16 +0200 |
wenzelm |
replaced Conv.goals_conv by Conv.prems_conv;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
exported meta_rewrite_conv;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:13 +0200 |
wenzelm |
removed obsolete eta_long_tac;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:13 +0200 |
wenzelm |
added CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
tuned rotate_prems;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:09 +0200 |
wenzelm |
removed obsolete mk_conjunction_list, intr/elim_list;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:09 +0200 |
wenzelm |
removed obsolete goals_conv (cf. prems_conv);
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:07 +0200 |
wenzelm |
Conjunction.intr/elim_balanced;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:07 +0200 |
wenzelm |
CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:06 +0200 |
wenzelm |
Conjunction.mk_conjunction_balanced;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:04 +0200 |
wenzelm |
CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 15:23:11 +0200 |
nipkow |
Fixed problem with patterns in lambdas
|
changeset |
files
|
| Tue, 03 Jul 2007 14:48:27 +0200 |
krauss |
fixed an issue with mutual recursion
|
changeset |
files
|
| Tue, 03 Jul 2007 01:26:06 +0200 |
huffman |
instance pordered_comm_ring < pordered_ring
|
changeset |
files
|
| Mon, 02 Jul 2007 23:14:06 +0200 |
nipkow |
Added pattern maatching for lambda abstraction
|
changeset |
files
|
| Mon, 02 Jul 2007 16:42:37 +0200 |
paulson |
revised the discussion of type classes
|
changeset |
files
|
| Mon, 02 Jul 2007 10:43:20 +0200 |
chaieb |
Generic QE need no Context anymore
|
changeset |
files
|
| Mon, 02 Jul 2007 10:43:19 +0200 |
chaieb |
Handle exception TYPE
|
changeset |
files
|
| Mon, 02 Jul 2007 10:43:17 +0200 |
chaieb |
Tuned proofs
|
changeset |
files
|
| Sat, 30 Jun 2007 17:30:10 +0200 |
obua |
added ordered_ring and ordered_semiring
|
changeset |
files
|
| Fri, 29 Jun 2007 21:23:05 +0200 |
haftmann |
tuned arithmetic modules
|
changeset |
files
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
changeset |
files
|
| Fri, 29 Jun 2007 16:05:00 +0200 |
haftmann |
dropped local cg cmd
|
changeset |
files
|
| Thu, 28 Jun 2007 19:09:43 +0200 |
haftmann |
dropped toplevel lcm, gcd
|
changeset |
files
|
| Thu, 28 Jun 2007 19:09:41 +0200 |
haftmann |
proper collapse_let
|
changeset |
files
|
| Thu, 28 Jun 2007 19:09:38 +0200 |
haftmann |
new code generator framework
|
changeset |
files
|
| Thu, 28 Jun 2007 19:09:36 +0200 |
haftmann |
dropped Library.lcm
|
changeset |
files
|
| Thu, 28 Jun 2007 19:09:35 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 28 Jun 2007 19:09:34 +0200 |
haftmann |
code generation for dvd
|
changeset |
files
|
| Thu, 28 Jun 2007 19:09:32 +0200 |
haftmann |
simplified keyword setup
|
changeset |
files
|
| Wed, 27 Jun 2007 12:41:36 +0200 |
paulson |
GPL -> BSD
|
changeset |
files
|
| Wed, 27 Jun 2007 11:06:43 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 26 Jun 2007 18:32:53 +0200 |
paulson |
updated for metis method
|
changeset |
files
|
| Tue, 26 Jun 2007 18:32:24 +0200 |
paulson |
recoded
|
changeset |
files
|
| Tue, 26 Jun 2007 18:28:40 +0200 |
paulson |
simplified
|
changeset |
files
|
| Tue, 26 Jun 2007 15:48:24 +0200 |
paulson |
completed some references
|
changeset |
files
|
| Tue, 26 Jun 2007 15:48:09 +0200 |
paulson |
changes for type class ring_no_zero_divisors
|
changeset |
files
|
| Tue, 26 Jun 2007 13:02:28 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 26 Jun 2007 13:01:48 +0200 |
nipkow |
added NBE
|
changeset |
files
|
| Tue, 26 Jun 2007 08:42:04 +0200 |
nipkow |
removed removed lemmas
|
changeset |
files
|