(* NOTE - this file linked multiple places, careful when editing *) structure OldGoals = Goals ; val () = ThyLoad.add_path "$ISABELLE_HOME_USER/2005/gen" ; val () = ThyLoad.add_path "$ISABELLE_HOME_USER/2005/pmgms" ; val () = ThyLoad.add_path "$ISABELLE_HOME_USER/2005/seqms" ; val () = ThyLoad.add_path "$ISABELLE_HOME/src/HOL/Lattice" ; val () = ThyLoad.add_path "$ISABELLE_HOME/src/HOL/Library" ; ThyLoad.show_path(); fun rmd _ = ThyInfo.remove_thy "bddefs" ; fun ud _ = ThyInfo.use_thy "bddefs" ; fun usq _ = ThyInfo.use_thy "bdseq" ; fun ulri _ = ThyInfo.use_thy "LRica" ; fun usb _ = ThyInfo.use_thy "LRisbcca" ; fun ubdl _ = ThyInfo.use_thy "bdlcons" ; fun ulti _ = ThyInfo.use_thy "LTitca" ; fun upi _ = ThyInfo.use_thy "pi" ; fun utau _ = ThyInfo.use_thy "tau" ; fun uhil _ = ThyInfo.use_thy "hilbert" ; fun udec _ = ThyInfo.use_thy "decidability" ; fun usbf _ = ThyInfo.use_thy "sb_finite" ; fun urb _ = ThyInfo.use_thy "wfrb" ; fun uk _ = ThyInfo.use_thy "konig" ; fun upst _ = ThyInfo.use_thy "pst" ; fun ua _ = ThyInfo.use_thy "all" ;