1994-07-15 |
clasohm |
added thy_name to Datatype_Fun's parameter
|
changeset |
files
|
1994-07-15 |
clasohm |
added check for concistency of filename and theory name;
|
changeset |
files
|
1994-07-15 |
clasohm |
added function mapst
|
changeset |
files
|
1994-07-14 |
wenzelm |
added functor signature constraint;
|
changeset |
files
|
1994-07-14 |
wenzelm |
minor internal renamings;
|
changeset |
files
|
1994-07-14 |
wenzelm |
changed syntax "(| _ : _ |)" to "OFCLASS(_, _)";
|
changeset |
files
|
1994-07-13 |
lcp |
indentation and renaming of rules
|
changeset |
files
|
1994-07-12 |
lcp |
minor updates
|
changeset |
files
|
1994-07-12 |
lcp |
chain_tac: deleted; just use etac mp
|
changeset |
files
|
1994-07-12 |
lcp |
Improved error checking
|
changeset |
files
|
1994-07-12 |
lcp |
new cardinal arithmetic developments
|
changeset |
files
|
1994-07-12 |
clasohm |
removed flatten_typ and replaced add_consts by add_consts_i
|
changeset |
files
|
1994-07-12 |
nipkow |
Corrected HOL.tex
|
changeset |
files
|
1994-07-12 |
nipkow |
added datatype section
|
changeset |
files
|
1994-07-12 |
nipkow |
included rail.sty
|
changeset |
files
|
1994-07-11 |
nipkow |
Initial revision
|
changeset |
files
|
1994-07-11 |
lcp |
minor edits
|
changeset |
files
|
1994-07-11 |
lcp |
restoring after deletion
|
changeset |
files
|
1994-07-11 |
lcp |
minor edits
|
changeset |
files
|
1994-07-11 |
nipkow |
type constraints
|
changeset |
files
|
1994-07-11 |
lcp |
documented subgoals_tac
|
changeset |
files
|
1994-07-11 |
lcp |
New errata list for the documentation
|
changeset |
files
|
1994-07-11 |
lcp |
misc updates
|
changeset |
files
|
1994-07-11 |
clasohm |
removed flatten_term and replaced add_axioms by add_axioms_i
|
changeset |
files
|
1994-07-07 |
nipkow |
added () around some of the ::
|
changeset |
files
|
1994-07-07 |
nipkow |
changed priority of ::
|
changeset |
files
|
1994-07-06 |
wenzelm |
exported opt_infix, opt_mixfix parsers;
|
changeset |
files
|
1994-07-06 |
wenzelm |
added raw_unify;
|
changeset |
files
|
1994-07-06 |
wenzelm |
various minor changes (names and comments);
|
changeset |
files
|
1994-07-06 |
clasohm |
changed comment for const_name
|
changeset |
files
|
1994-07-06 |
wenzelm |
changed comment only;
|
changeset |
files
|
1994-07-01 |
clasohm |
rewritec now uses trace_thm for it's "rewrite rule from different theory"
|
changeset |
files
|
1994-07-01 |
clasohm |
changed syntax of datatype declaration
|
changeset |
files
|
1994-07-01 |
clasohm |
replaced extend_theory by new add_* functions;
|
changeset |
files
|
1994-06-29 |
clasohm |
added parentheses made necessary by new constrain precedence
|
changeset |
files
|
1994-06-29 |
clasohm |
added parentheses made necessary by change of constrain's precedence
|
changeset |
files
|
1994-06-29 |
clasohm |
changed precedence of constrain to [4, 0], 3
|
changeset |
files
|
1994-06-24 |
lcp |
FOL/FOL.ML/excluded_middle_tac: new
|
changeset |
files
|
1994-06-24 |
lcp |
Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
|
changeset |
files
|
1994-06-23 |
lcp |
minor tidying up (ordered rewriting in Integ.ML)
|
changeset |
files
|
1994-06-23 |
lcp |
modifications for cardinal arithmetic
|
changeset |
files
|
1994-06-23 |
lcp |
Sara\'s perl script for renaming theory files
|
changeset |
files
|
1994-06-21 |
lcp |
Addition of cardinals and order types, various tidying
|
changeset |
files
|
1994-06-21 |
lcp |
Various updates and tidying
|
changeset |
files
|
1994-06-21 |
nipkow |
improved error msg
|
changeset |
files
|
1994-06-20 |
nipkow |
Improved error msg "Proved wrong thm"
|
changeset |
files
|
1994-06-20 |
clasohm |
parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
|
changeset |
files
|
1994-06-20 |
nipkow |
Franz Regensburger's changes.
|
changeset |
files
|
1994-06-17 |
lcp |
atomize: borrowed HOL version, which checks for both Trueprop
|
changeset |
files
|
1994-06-17 |
lcp |
problem 38 is provable
|
changeset |
files
|
1994-06-17 |
nipkow |
ordered rewriting applies to conditional rules as well now
|
changeset |
files
|
1994-06-17 |
clasohm |
replaced "foldl merge_theories" by "merge_thy_list" in base_on
|
changeset |
files
|
1994-06-16 |
wenzelm |
added 'subclass' section;
|
changeset |
files
|
1994-06-16 |
wenzelm |
base_on: added 'mk_draft' arg;
|
changeset |
files
|
1994-06-16 |
wenzelm |
(beta release)
|
changeset |
files
|
1994-06-16 |
wenzelm |
added ext_tsig_subclass, ext_tsig_defsort;
|
changeset |
files
|
1994-06-16 |
wenzelm |
added add_classrel;
|
changeset |
files
|
1994-06-09 |
wenzelm |
replaced extend_theory;
|
changeset |
files
|
1994-06-09 |
wenzelm |
added OldMixfix;
|
changeset |
files
|
1994-06-09 |
wenzelm |
workaround bug in Type.expand_typ;
|
changeset |
files
|