TFL/README
author paulson
Mon, 23 Jun 1997 11:30:35 +0200
changeset 3458 5ff4bfab859c
parent 3191 14bd6e5985f1
permissions -rw-r--r--
Removal of COND_CONG, which is just if_cong RS eq_reflection
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";  
3191
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
     5
3. cd "examples/Subst";      or 3. cd "examples";
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
     6
4. use "ROOT.ML";               4. use"test.sml";