Old_HOL: Graph

Mercurial Mercurial > repos > Old_HOL / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -100 -60 +60 tip

adapted to 'subtype' section;
1994-11-25, by wenzelm
added id_in_pair_conv
1994-11-25, by nipkow
Removed obsolete induction package
1994-11-25, by nipkow
removed Sum-rules
1994-11-25, by nipkow
checks that the recursive sets are Consts before taking
1994-11-25, by lcp
renamed term_induct/2 -> Term_induct/2
1994-11-25, by nipkow
replaced prove_goal by qed_goal
1994-11-25, by clasohm
rules -> defs
1994-11-24, by nipkow
The collection of theories required for inductive definitions.
1994-11-24, by nipkow
Trancl.{thy,ML} was missing
1994-11-24, by nipkow
moved parser stuff to thy_syntax.ML;
1994-11-23, by wenzelm
add_subtype now adds constant definition for the representing set;
1994-11-23, by wenzelm
moved remaining thy syntax stuff to thy_syntax.ML;
1994-11-23, by wenzelm
added 'datatype' and 'primrec';
1994-11-23, by wenzelm
replaced 'val ... = result()' by 'qed "..."'
1994-11-21, by clasohm
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
1994-11-11, by lcp
Initial revision
1994-11-10, by nipkow
Added headers and made various small mods.
1994-11-09, by nipkow
Added header.
1994-11-09, by nipkow
HOL/ROOT/HOL_dup_cs: removed as obsolete
1994-11-08, by lcp
changed loadpath
1994-11-06, by clasohm
changed command for making 'test'
1994-11-06, by clasohm
rearranged theory section stuff;
1994-11-04, by wenzelm
moved section parser to thy_syntax.ML;
1994-11-04, by wenzelm
lnternal interface for HOL subtype definitions;
1994-11-04, by wenzelm
additional theory file sections for HOL;
1994-11-04, by wenzelm
abstract syntax operations for HOL;
1994-11-04, by wenzelm
Replaced fast_tac by simp_tac in a number of places.
1994-11-03, by nipkow
added IOA files
1994-11-02, by clasohm
added IOA to isabelle/HOL
1994-11-02, by clasohm
HOL/HOL/swap: deleted
1994-11-01, by lcp
HOL/ex/cla: proofs now use deepen_tac instead of best_tac HOL_dup_cs
1994-10-31, by lcp
HOL/HOL.ML/selectI2: new rule for descriptions
1994-10-13, by lcp
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
1994-10-12, by lcp
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
1994-10-12, by lcp
replaced some "rules" by "defs"
1994-10-06, by nipkow
changed precedences to eliminate some ambiguities Isabelle94-1
1994-10-04, by clasohm
moved LList* to ex
1994-09-28, by nipkow
Small simplification in add_datatype.
1994-09-27, by nipkow
replaced local instantaite_types by inferT_axm
1994-09-26, by nipkow
minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections;
1994-09-21, by wenzelm
Definition of C was not truly prim rec because C was called inside Gamma
1994-09-16, by nipkow
improved error reporting for primrec
1994-09-15, by nipkow
replaced lookup_const by Sign.const_type; Isabelle94
1994-09-14, by wenzelm
Allowed string as function name in primrec header
1994-09-11, by nipkow
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
1994-09-08, by lcp
HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster
1994-09-07, by lcp
changed names
1994-09-06, by nipkow
Converted rules to primrecs
1994-09-06, by nipkow
corrected comment re treatment of types such as (bool*bool)*bool
1994-09-06, by lcp
HOL/ex/PropLog.thy: tidied
1994-09-06, by lcp
HOL/ind_syntax/factors: now returns only factors in the product type that
1994-09-06, by lcp
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
1994-08-31, by nipkow
Renamed a few types and vars
1994-08-31, by nipkow
Equivalence of op. and den. sem. for simple while language.
1994-08-31, by nipkow
Updated PL to PropLog using Larrys ind. defs.
1994-08-30, by nipkow
New version of datatype.ML with primrec (Norbert).
1994-08-30, by nipkow
INSTALLATION OF INDUCTIVE DEFINITIONS
1994-08-25, by lcp
INSTALLATION OF INDUCTIVE DEFINITIONS
1994-08-25, by lcp
Subst/UTerm: updated for inductive defs; streamlined proofs
1994-08-24, by lcp

less more | (0) -100 -60 +60 tip

Old_HOL