1996-04-27 nipkow 1996-04-27 Added R^1 = R
1996-04-26 paulson 1996-04-26 Renaming of a lemma
1996-04-26 paulson 1996-04-26 Fixed indenting
1996-04-26 clasohm 1996-04-26 added changes by Konrad to prove_nchotomy
1996-04-25 paulson 1996-04-25 Fixed some unfortunate variable names
1996-04-25 paulson 1996-04-25 Now contains HOLCF
1996-04-25 oheimb 1996-04-25 temporarily included settings for unification bounds again
1996-04-25 berghofe 1996-04-25 Added functions mk_cntxt_splitthm and inst_split which instantiate the split-rule before it is applied. Inserted some comments.
1996-04-25 paulson 1996-04-25 Fixed a silly variable name
1996-04-25 paulson 1996-04-25 Rearrangement and polishing to look for for publication
1996-04-25 paulson 1996-04-25 Now calls "rail" to update datatype syntax charts
1996-04-25 paulson 1996-04-25 automatic updates
1996-04-24 oheimb 1996-04-24 changed two goals formulated with 8bit font
1996-04-24 clasohm 1996-04-24 removed David's private version (i.e. restored version 1.1)
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets,
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-23 oheimb 1996-04-23 adapted several proofs
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
1996-04-23 oheimb 1996-04-23 included (empty) test goal for symmetry reasons
1996-04-23 clasohm 1996-04-23 use_dir and exit_use_dir now change the CWD only temporarily
1996-04-22 nipkow 1996-04-22 inserted Suc_less_eq explictly in a few proofs. inserted o_def explictly in a few proofs because the new split_tac causes fewer eta-expansions which some of the rewrites need. Indented proof in I.ML
1996-04-19 clasohm 1996-04-19 added Konrad's code for the datatype package
1996-04-19 clasohm 1996-04-19 adapted to new version of Fun.ML
1996-04-19 clasohm 1996-04-19 removed assignment of HOL_ss to simpset
1996-04-19 clasohm 1996-04-19 added thy_data.ML
1996-04-19 clasohm 1996-04-19 added thyname_of_sign (used in HOL/thy_data.ML)
1996-04-18 oheimb 1996-04-18 adapted proof of drop_succ_Cons: problem with non-confluent simpset removed
1996-04-18 oheimb 1996-04-18 adapted proof of less_succ: problem because of non-confluent SimpSet removed
1996-04-18 oheimb 1996-04-18 *** empty log message ***
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-12 clasohm 1996-04-12 add_thydata and get_thydata now take a string as their first argument
1996-04-12 clasohm 1996-04-12 changed first parameter of add_thydata and get_thydata
1996-04-11 clasohm 1996-04-11 fixed bug in set_current_thy
1996-04-11 nipkow 1996-04-11 Added a number of lemmas
1996-04-09 berghofe 1996-04-09 select_match now sorts list of matching theorems according to the number of premises and size of the required substitution
1996-04-04 nipkow 1996-04-04 Replaced !simpset by HOL_ss on line 93.
1996-04-04 paulson 1996-04-04 Proved Inter_0 and converse_INT
1996-04-04 paulson 1996-04-04 deleted obsolete comment
1996-04-04 nipkow 1996-04-04 Added 'constdefs'
1996-04-04 nipkow 1996-04-04 Added 'constdefs' and extended the section on 'defs'
1996-04-04 nipkow 1996-04-04 Messed up last update.
1996-04-04 nipkow 1996-04-04 Replaced \CHOL by \HOLCF
1996-04-04 paulson 1996-04-04 updated comments
1996-04-04 nipkow 1996-04-04 Moved link to paper.
1996-04-04 oheimb 1996-04-04 Removed 8bit characters used by mistake
1996-04-04 paulson 1996-04-04 Fixed error in CHANGED (caused by variable renaming)
1996-04-04 paulson 1996-04-04 Using new "Times" infix
1996-04-04 paulson 1996-04-04 For renaming to rtrancl_Un_rtrancl
1996-04-04 paulson 1996-04-04 Added more _iff rewrites for Compl, Un, Int
1996-04-04 paulson 1996-04-04 New example Comb: Church-Rosser for combinators, ported from ZF
1996-04-03 oheimb 1996-04-03 *** empty log message ***
1996-04-03 oheimb 1996-04-03 Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
1996-04-03 nipkow 1996-04-03 Introduced Times and SIGMA.
1996-04-03 oheimb 1996-04-03 *** empty log message ***
1996-04-03 nipkow 1996-04-03 Plugged some more loopholes with nodup_Vars.