TFL/README
author nipkow
Fri, 07 Feb 1997 14:15:35 +0100
changeset 2597 8b523426e1a4
parent 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
Modified proofs due to added triv_forall_equality.
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";