Old_HOL: Graph

Mercurial Mercurial > repos > Old_HOL / graph

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

Added Id: line
1995-04-06, by lcp
replaced 'arities' by 'instance';
1995-03-31, by wenzelm
Defined addss to perform simplification in a claset.
1995-03-30, by lcp
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
1995-03-28, by clasohm
Added recursion equations for foldl to list_ss.
1995-03-27, by nipkow
Added a few thms to nat_ss and list_ss
1995-03-17, by nipkow
Now calls exit_use instead of use, for prompt failure if errors are detected.
1995-03-15, by lcp
Removed some type constraints
1995-03-14, by nipkow
added "exit 1"
1995-03-14, by nipkow
Removed unecessary type constraint because instantiations do not freeze type
1995-03-13, by nipkow
Added dependencies on ../Provers/hypsubst.ML and removed those on
1995-03-08, by nipkow
Enforced partial evaluation of mk_case_split_tac
1995-03-08, by nipkow
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
1995-03-01, by lcp
Proofs of inv1 and inv4 now use less_le_trans instead of
1995-03-01, by lcp
Renamed plus_leD1 to add_leD1.
1995-03-01, by lcp
Proved inj_onto_iff
1995-03-01, by lcp
No longer calls maketest; instead, the Makefile writes the file
1995-02-28, by lcp
Re-organised to perform the tests independently. Now test
1995-02-28, by lcp
Installation of Integ (ported from ZF by Mattolini)
1995-02-28, by lcp
Proved less_eq_Suc_add and add_left_cancel (cf left_plus_cancel on
1995-02-28, by lcp
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
1995-02-27, by lcp
Installation of Integ (ported from ZF by Mattolini)
1995-02-27, by lcp
Installation of Integ (ported from ZF by Mattolini)
1995-02-27, by lcp
Reorganized/optimized datatype definitions.
1995-02-19, by nipkow
pair_ss -> prod_ss.
1995-02-16, by nipkow
Removed pair_ss because identical to prod_ss.
1995-02-16, by nipkow
Added "flat"
1995-02-13, by nipkow
Norbert's update allowing nested calls in primrec.
1995-02-08, by nipkow
More rewrite rules.
1995-02-08, by nipkow
Add dependence on ex/String.thy/ML
1995-02-03, by nipkow
Added Markus Wenzel's string representation.
1995-02-03, by nipkow
Simplified proof.
1995-02-01, by nipkow
The thm if(P,Q,R) now yields the two conditional rewrite rules P ==> Q and
1995-02-01, by nipkow
Added Un_empty (also to set_ss)
1995-01-30, by nipkow
Added some simplifications for ? x.
1995-01-29, by nipkow
Added "nth" and some lemmas.
1995-01-26, by nipkow
added bind_thm for theorems made by "standard ..." Isabelle94-2
1994-12-14, by clasohm
improved primrec: now calls store_thm;
1994-12-14, by wenzelm
removed HOL_Lemmas structure and added qed_goal
1994-12-09, by clasohm
replaced store_thm by bind_thm
1994-12-08, by clasohm
Added (? x. x=t & P) = P to the simpset.
1994-12-07, by nipkow
Removed a local lemma which is now part of HOL_ss.
1994-12-07, by nipkow
Moved the old List to ex and replaced it by one defined via
1994-12-02, by nipkow
Moved HOL/List to HOL/ex/SList (strict list).
1994-12-02, by nipkow
small updates because datatype list is now used. In particular Nil -> []
1994-12-02, by nipkow
list_ind_tac -> list.induct_tac
1994-12-02, by nipkow
Added dependency on thy_syntax.ML
1994-12-01, by nipkow
Fixed small bug in print-translation for set comprehension.
1994-11-28, by nipkow
adapted to 'subtype' section;
1994-11-28, by wenzelm
added IMP/Properties
1994-11-25, by nipkow
Proved determinism.
1994-11-25, by nipkow
minor changes according to new hologic;
1994-11-25, by wenzelm
replaced ["term"] by termS;
1994-11-25, by wenzelm
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

less more | (0) -100 -60 tip

Old_HOL