Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] View of /sml/trunk/src/eXene/demos/tactic-tree/examples/hol/README
ViewVC logotype

View of /sml/trunk/src/eXene/demos/tactic-tree/examples/hol/README

Parent Directory Parent Directory | Revision Log Revision Log

Revision 651 - (download) (annotate)
Thu Jun 1 18:34:03 2000 UTC (19 years, 3 months ago) by monnier
File size: 1713 byte(s)
bring revisions from the vendor branch to the trunk
		HOL with tactic trees. 

Files in this directory: 

	hol-support.sml      : structure used to build tactic tree interface on top of HOL
        make-interactive.sml : builds interactive version of tactic tree interface 

It is assumed that all of the tactic_tree/src/ files have already been read into eXene. 
This is meant to be built on top of version SML New Jersey version of HOL, 
(for information contact Elsa Gunter, elsa@research.att.com) that has been 
been built on top of eXene, or had eXene built on top of it. 

The interactive version of tactic trees for HOL provides the following functions: 
create : term * string * string list -> ttree_state

	create(f,s,l) opens up a window with term f as the top-level
        goal (no assumptions) on display s with tactic menu extension l. 
        l is a list of strings -- each should parse to an ML value of type 
	tactic.  s is a string that tells the X server which screen you want 
        the window to pop up on. Check your unix envrironment variable DISPLAY. 

view : ttree_state * string * string list -> ttree_state

	view(p,s,l) opens up a window for tactic-tree state p 
        on display s with tactic menu extension l. 
extract_event : ttree_state -> thm 

	extract_event p will return the HOL thm proved by the tactic-tree in state
	p. Assumes that all subgoals have been proven. 

extract_tactic : ttree_state -> string 

	extract_tactic p will return a string representing the HOL tactic that if 
	applied to the top-level goal will produce the fringe (unproven subgoals) 
        of the tactic tree. 

extract_text : ttree_state -> string -> unit

	extract_text p s writes the tree represented by p to the file s. 

ViewVC Help
Powered by ViewVC 1.0.0