Sat, 29 May 2004 15:05:25 +0200 |
wenzelm |
removed norm_typ; improved output; refer to Pretty.pp;
|
changeset |
files
|
Sat, 29 May 2004 15:05:02 +0200 |
wenzelm |
moved read_int etc. to library.ML; added type 'arity';
|
changeset |
files
|
Sat, 29 May 2004 15:03:59 +0200 |
wenzelm |
improved output; refer to Pretty.pp;
|
changeset |
files
|
Sat, 29 May 2004 15:02:35 +0200 |
wenzelm |
Output.add_mode; Output.timing;
|
changeset |
files
|
Sat, 29 May 2004 15:02:13 +0200 |
wenzelm |
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
|
changeset |
files
|
Sat, 29 May 2004 15:01:36 +0200 |
wenzelm |
Output.timing;
|
changeset |
files
|
Sat, 29 May 2004 15:00:52 +0200 |
wenzelm |
improved output;
|
changeset |
files
|
Sat, 29 May 2004 15:00:25 +0200 |
wenzelm |
moved print_mode to General/output.ML; load General/pretty.ML early;
|
changeset |
files
|
Sat, 29 May 2004 15:00:14 +0200 |
wenzelm |
added Pure/General/output.ML;
|
changeset |
files
|
Sat, 29 May 2004 14:59:57 +0200 |
wenzelm |
avoid 'handle _' -- would cover Interrupt as well!!!
|
changeset |
files
|
Sat, 29 May 2004 14:59:24 +0200 |
wenzelm |
Sign.infer_types: Sign.pp;
|
changeset |
files
|
Sat, 29 May 2004 14:58:44 +0200 |
wenzelm |
Library.read_int;
|
changeset |
files
|
Sat, 29 May 2004 14:57:39 +0200 |
wenzelm |
Output.output;
|
changeset |
files
|
Sat, 29 May 2004 14:55:56 +0200 |
wenzelm |
'classrel': support multiple arguments;
|
changeset |
files
|
Sat, 29 May 2004 14:54:58 +0200 |
wenzelm |
* ML: all output via channels of writeln etc. passed through Output.output;
|
changeset |
files
|
Sat, 29 May 2004 14:54:10 +0200 |
wenzelm |
output channels;
|
changeset |
files
|
Fri, 28 May 2004 21:09:56 +0200 |
schirmer |
added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
|
changeset |
files
|
Fri, 28 May 2004 11:20:04 +0200 |
paulson |
new skolemize_tac and skolemize method
|
changeset |
files
|
Fri, 28 May 2004 11:19:15 +0200 |
paulson |
new theorem Collect_imp_eq
|
changeset |
files
|
Wed, 26 May 2004 19:06:09 +0200 |
chaieb |
abstraction over functions is no default any more.
|
changeset |
files
|
Wed, 26 May 2004 18:52:18 +0200 |
webertj |
adjusted for different signature of Type.typ_instance
|
changeset |
files
|
Wed, 26 May 2004 18:23:46 +0200 |
webertj |
mainly new/different datatype examples
|
changeset |
files
|
Wed, 26 May 2004 18:06:38 +0200 |
webertj |
documentation updated
|
changeset |
files
|
Wed, 26 May 2004 18:03:52 +0200 |
webertj |
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
|
changeset |
files
|
Wed, 26 May 2004 17:43:52 +0200 |
webertj |
new default parameters for refute
|
changeset |
files
|
Wed, 26 May 2004 17:42:46 +0200 |
webertj |
solver "auto" now issues a warning when it uses solver "enumerate"
|
changeset |
files
|
Wed, 26 May 2004 14:57:06 +0200 |
nipkow |
Corrected printer bug for bounded quantifiers Q x<=y. P
|
changeset |
files
|
Wed, 26 May 2004 11:43:50 +0200 |
paulson |
more group isomorphisms
|
changeset |
files
|
Mon, 24 May 2004 18:35:34 +0200 |
nipkow |
added drop_take:thm
|
changeset |
files
|
Fri, 21 May 2004 21:49:45 +0200 |
berghofe |
- deleted unneeded function eta_long (now in Pure/pattern.ML
|
changeset |
files
|