| 2008-06-28 |
wenzelm |
added macro interface;
|
changeset |
files
|
| 2008-06-28 |
wenzelm |
tuned;
|
changeset |
files
|
| 2008-06-28 |
wenzelm |
added thm_name, opt_thm_name;
|
changeset |
files
|
| 2008-06-27 |
haftmann |
adjusted import
|
changeset |
files
|
| 2008-06-27 |
haftmann |
adjusted import
|
changeset |
files
|
| 2008-06-26 |
urbanc |
added a lemma to at_swap_simps
|
changeset |
files
|
| 2008-06-26 |
huffman |
remove cset theory; define ideal completions using typedef instead of cpodef
|
changeset |
files
|
| 2008-06-26 |
wenzelm |
Args.theory;
|
changeset |
files
|
| 2008-06-26 |
wenzelm |
added context/theory scanner;
|
changeset |
files
|
| 2008-06-26 |
wenzelm |
Args.context;
|
changeset |
files
|
| 2008-06-26 |
krauss |
fix: need to beta/eta normalize
|
changeset |
files
|
| 2008-06-26 |
haftmann |
established Plain theory and image
|
changeset |
files
|
| 2008-06-26 |
haftmann |
added dummy citiation
|
changeset |
files
|
| 2008-06-26 |
haftmann |
dropped recdef
|
changeset |
files
|
| 2008-06-26 |
haftmann |
class theory name lookup improved
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| 2008-06-25 |
urbanc |
typo
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
re-use official outer keywords;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
scan: prefer command over keyword, allowing lexicons to overlap;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
antiquote: need to quote outer keywords;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
tuned;
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
changeset |
files
|
| 2008-06-25 |
berghofe |
- Equivariance simpset used in proofs of strong induction and inversion
|
changeset |
files
|
| 2008-06-25 |
wenzelm |
pprint: back to proper output of markup, with workaround for Poly/ML crash;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
back to 1.36 (Poly/ML crash!?);
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
updated generated file;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
YXML: no special treatment of white space;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
pprint: proper output of markup (important for token translation);
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
ml_code_antiq: proper scanner combinators;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
moved concrete antiquotations to ml_antiquote.ML;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
Antiquote.Open/Close;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
add_antiq: more general notion of ML antiquotation;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
added Open/Close -- checked blocks;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
added pprint_thy_ref;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
Common ML antiquotations.
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
added ML/ml_antiquote.ML;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
ML_Antiquote.value;
|
changeset |
files
|
| 2008-06-24 |
wenzelm |
added isaantiqopen/close;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
moved implies to logic.ML;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
added all, is_all;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
Logic.implies;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
Logic.is_all;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
Term.all;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
session name: empty for Pure and by default;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
induct_tac: allow omission of arguments;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
info: default name is "", not "Pure";
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
removed obsolete dest_concls;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
induct_tac: mutual rules work as for method "induct";
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
tuned get_inductT: *all* rules for missing instantiation;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
induct_tac: infer mutual rule from types, as for proper induct method;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
induct_tac/case_tac: nested tuples are split as expected;
|
changeset |
files
|
| 2008-06-23 |
wenzelm |
induct_tac: old conjunctive rules no longer supported;
|
changeset |
files
|