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

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOL/Subst/ROOT.ML
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 9000 diff changeset	2	Authors: Martin Coen, Cambridge University Computer Laboratory
261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 9000 diff changeset	3	Konrad Slind, TU Munich
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	4	Copyright 1993 University of Cambridge,
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	5	1996 TU Munich
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	6
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	7	Substitution and Unification in Higher-Order Logic.
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	8
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	9	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	10	and some new simplifications by Slind.
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	11
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	12	Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm.
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	13	SCP 1 (1981), 5-48
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	14
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	15	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	16
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	17	AList - association lists
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	18	UTerm - data type of terms
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	19	Subst - substitutions
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	20	Unifier - specification of unification and conditions for
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	21	correctness and termination
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	22	Unify - the unification function
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	23
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	24	*)
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	25
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 9000 diff changeset	26	use_thys ["Unify"];

author	blanchet
	Wed, 28 Apr 2010 18:11:11 +0200
changeset 36550	f8da913b6c3a
parent 33615	261abc2e3155
permissions	-rw-r--r--