| Sat, 07 Jul 2007 18:39:16 +0200 |
wenzelm |
use markup.ML earlier;
|
changeset |
files
|
| Sat, 07 Jul 2007 18:39:15 +0200 |
wenzelm |
removed obsolete disable_pr/enable_pr;
|
changeset |
files
|
| Sat, 07 Jul 2007 18:39:14 +0200 |
wenzelm |
pretty_goals_aux: subgoal markup;
|
changeset |
files
|
| Sat, 07 Jul 2007 18:39:12 +0200 |
wenzelm |
pr_goals: adapted Display.pretty_goals_aux;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:20 +0200 |
wenzelm |
export attribute;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:19 +0200 |
wenzelm |
pretty_sort/typ/term: markup;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:18 +0200 |
wenzelm |
pretty: markup for syntax/name of authentic consts;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:17 +0200 |
wenzelm |
depend on alist.ML, markup.ML;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:16 +0200 |
wenzelm |
markup: emit as control information -- no indent text;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:15 +0200 |
wenzelm |
added property conversions;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:14 +0200 |
wenzelm |
position: line and name;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:13 +0200 |
wenzelm |
moved markup.ML before position.ML;
|
changeset |
files
|
| Sat, 07 Jul 2007 11:09:40 +0200 |
chaieb |
The order for parameter for interpretation is now inversted:
|
changeset |
files
|
| Sat, 07 Jul 2007 00:17:10 +0200 |
wenzelm |
Common markup elements.
|
changeset |
files
|
| Sat, 07 Jul 2007 00:15:03 +0200 |
wenzelm |
simplified pretty token metric: type int;
|
changeset |
files
|
| Sat, 07 Jul 2007 00:15:02 +0200 |
wenzelm |
simplified pretty token metric: type int;
|
changeset |
files
|
| 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
|