isabelle: src/HOL/Subst/ROOT.ML@572a483de1b0 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOL/Subst/ROOT.ML
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1165 diff changeset	2	ID: $Id$
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	3	Authors: Martin Coen, Cambridge University Computer Laboratory
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	4	Konrad Slind, TU Munich
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	5	Copyright 1993 University of Cambridge,
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	6	1996 TU Munich
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	7
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	8	Substitution and Unification in Higher-Order Logic.
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	9
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	10	Implements Manna & Waldinger's formalization, with Paulson's simplifications,
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	11	and some new simplifications by Slind.
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	12
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	13	Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm.
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	14	SCP 1 (1981), 5-48
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	15
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	16	L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	17
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	18	AList - association lists
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	19	UTerm - data type of terms
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	20	Subst - substitutions
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	21	Unifier - specification of unification and conditions for
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	22	correctness and termination
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	23	Unify - the unification function
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	24
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	25	*)
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	26
9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	27	time_use_thy "Unify";

author	wenzelm
	Tue, 05 Jun 2007 22:46:55 +0200
changeset 23268	572a483de1b0
parent 9000	c20d58286a51
child 33615	261abc2e3155
permissions	-rw-r--r--