TFL/README
author paulson
Wed, 02 Apr 1997 15:14:37 +0200
changeset 2865 77daca16b2f4
parent 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
ZF.thy is again usable
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     1
How to build TFL and run the Unify example.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     2
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     3
1. Invoke the current version of Isabelle-HOL.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     4
2. use "sys.sml";  
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     5
3. cd examples/Subst
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     6
4. use "ROOT.ML";