equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/Follows.thy |
1 (* Title: HOL/UNITY/Follows.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header{*The Follows Relation of Charpentier and Sivilotte*} |
6 section{*The Follows Relation of Charpentier and Sivilotte*} |
7 |
7 |
8 theory Follows |
8 theory Follows |
9 imports SubstAx ListOrder "~~/src/HOL/Library/Multiset" |
9 imports SubstAx ListOrder "~~/src/HOL/Library/Multiset" |
10 begin |
10 begin |
11 |
11 |