haftmann [Fri, 13 Mar 2009 19:17:58 +0100] rev 30519
coherent binding policy with primitive target operations
haftmann [Fri, 13 Mar 2009 19:17:57 +0100] rev 30518
moved some generic nonsense to arith_data.ML
haftmann [Fri, 13 Mar 2009 19:17:57 +0100] rev 30517
tuned ML code
huffman [Fri, 13 Mar 2009 10:14:47 -0700] rev 30516
remove legacy ML bindings
wenzelm [Fri, 13 Mar 2009 23:50:05 +0100] rev 30515
simplified method setup;
wenzelm [Fri, 13 Mar 2009 23:32:40 +0100] rev 30514
simplified goal_spec: default to first goal;
wenzelm [Fri, 13 Mar 2009 21:25:15 +0100] rev 30513
eliminated type Args.T;
pervasive types 'a parser and 'a context_parser;
wenzelm [Fri, 13 Mar 2009 21:24:21 +0100] rev 30512
added simplified setup;
eliminated type Args.T;
pervasive types 'a parser and 'a context_parser;
wenzelm [Fri, 13 Mar 2009 21:22:45 +0100] rev 30511
pervasive types 'a parser and 'a context_parser;
wenzelm [Fri, 13 Mar 2009 19:58:26 +0100] rev 30510
unified type Proof.method and pervasive METHOD combinators;
wenzelm [Fri, 13 Mar 2009 19:53:09 +0100] rev 30509
more regular method setup via SIMPLE_METHOD;
wenzelm [Fri, 13 Mar 2009 19:10:46 +0100] rev 30508
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm [Fri, 13 Mar 2009 15:52:23 +0100] rev 30507
merged
huffman [Fri, 13 Mar 2009 07:35:18 -0700] rev 30506
fix typed print translation for CARD('a)
huffman [Fri, 13 Mar 2009 07:30:47 -0700] rev 30505
introduce new helper functions; clean up proofs
nipkow [Fri, 13 Mar 2009 13:06:36 +0100] rev 30504
merged
nipkow [Fri, 13 Mar 2009 13:06:00 +0100] rev 30503
added comment
nipkow [Fri, 13 Mar 2009 12:32:29 +0100] rev 30502
hiding numeric coercions in LaTeX
haftmann [Fri, 13 Mar 2009 12:29:38 +0100] rev 30501
merged
haftmann [Fri, 13 Mar 2009 08:16:18 +0100] rev 30500
dropped spurious `quote` tags
haftmann [Thu, 12 Mar 2009 23:01:25 +0100] rev 30499
merged
haftmann [Thu, 12 Mar 2009 18:01:27 +0100] rev 30498
tuned
haftmann [Thu, 12 Mar 2009 18:01:26 +0100] rev 30497
strippd Id
haftmann [Thu, 12 Mar 2009 18:01:26 +0100] rev 30496
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann [Thu, 12 Mar 2009 18:01:25 +0100] rev 30495
tuned
haftmann [Thu, 12 Mar 2009 18:01:25 +0100] rev 30494
consider exit status of code generation direcitve
wenzelm [Fri, 13 Mar 2009 15:50:06 +0100] rev 30493
provide regular ML interfaces for Isar source language elements;
wenzelm [Fri, 13 Mar 2009 15:50:05 +0100] rev 30492
get data from plain Proof.context;